:: HAUSDORF semantic presentation begin registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); cluster (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "M") -> ($#v8_pre_topc :::"T_2"::: ) ; end; theorem :: HAUSDORF:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: HAUSDORF:2 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: HAUSDORF:3 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "x")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))))))) ; theorem :: HAUSDORF:4 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "x")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: HAUSDORF:5 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: HAUSDORF:6 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ))) ")" )))) ; theorem :: HAUSDORF:7 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ))) ")" )))) ; theorem :: HAUSDORF:8 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "P")))) "iff" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: HAUSDORF:9 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) "iff" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: HAUSDORF:10 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "ex" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k3_weierstr :::"lower_bound"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X")))) ")" ))) ; theorem :: HAUSDORF:11 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "ex" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k2_weierstr :::"upper_bound"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "X")))) ")" ))) ; theorem :: HAUSDORF:12 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "x")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ))))) ; theorem :: HAUSDORF:13 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))))) ; theorem :: HAUSDORF:14 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) ")" )) "holds" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))))))) ; theorem :: HAUSDORF:15 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" )))))) ; theorem :: HAUSDORF:16 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q")))) "holds" (Bool (Set (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" (Set (Var "M")) ($#k1_topmetr :::"|"::: ) (Set (Var "Q")) ")" )))))) ; theorem :: HAUSDORF:17 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "M")) ($#k1_topmetr :::"|"::: ) (Set (Var "B")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) "is" ($#v6_tbsp_1 :::"bounded"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v6_tbsp_1 :::"bounded"::: ) ))))) ; theorem :: HAUSDORF:18 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Var "B")) "is" ($#v6_tbsp_1 :::"bounded"::: ) )))) ; theorem :: HAUSDORF:19 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "w")) "," (Set (Var "z")) ")" )) ")" ))))) ; registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); cluster (Set ($#k4_weierstr :::"dist"::: ) "x") -> ($#v5_pre_topc :::"continuous"::: ) ; end; registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Const "M")) ")" ); cluster (Set ($#k5_weierstr :::"dist_max"::: ) "X") -> ($#v5_pre_topc :::"continuous"::: ) ; cluster (Set ($#k6_weierstr :::"dist_min"::: ) "X") -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: HAUSDORF:20 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Set "(" ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))))) ; theorem :: HAUSDORF:21 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "w")) "," (Set (Var "z")) ")" )) ")" ))))) ; theorem :: HAUSDORF:22 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_weierstr :::"max_dist_max"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ))))) ; theorem :: HAUSDORF:23 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Set "(" ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_weierstr :::"max_dist_max"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ))))) ; theorem :: HAUSDORF:24 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q")))) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )))) ; theorem :: HAUSDORF:25 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q")))) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )))) ; theorem :: HAUSDORF:26 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))))))) ; theorem :: HAUSDORF:27 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "holds" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_seq_4 :::"}"::: ) )))) ; theorem :: HAUSDORF:28 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: HAUSDORF:29 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "holds" (Bool (Set ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "P")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: HAUSDORF:30 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set ($#k9_weierstr :::"min_dist_max"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: HAUSDORF:31 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "Q")) "," (Set (Var "R")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "R")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "R")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "R")) "," (Set (Var "Q")) ")" ))))) ; begin definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "P", "Q" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Const "M")) ")" ); func :::"HausDist"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Real":::) equals :: HAUSDORF:def 1 (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" ($#k8_weierstr :::"max_dist_min"::: ) "(" "P" "," "Q" ")" ")" ) "," (Set "(" ($#k8_weierstr :::"max_dist_min"::: ) "(" "Q" "," "P" ")" ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Const "M")) ")" ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) "," (Set "(" ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "Q")) "," (Set (Var "P")) ")" ")" ) ")" ))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "Q")) "," (Set (Var "P")) ")" ")" ) "," (Set "(" ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) ")" )))) ; end; :: deftheorem defines :::"HausDist"::: HAUSDORF:def 1 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "holds" (Bool (Set ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) "," (Set "(" ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "Q")) "," (Set (Var "P")) ")" ")" ) ")" )))); theorem :: HAUSDORF:32 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "Q")) "," (Set (Var "R")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "R")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "R")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "Q")) "," (Set (Var "R")) ")" ))))) ; theorem :: HAUSDORF:33 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "R")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "P")) "," (Set (Var "R")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "Q")) "," (Set (Var "R")) ")" ")" ))))) ; theorem :: HAUSDORF:34 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "R")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "R")) "," (Set (Var "P")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "Q")) "," (Set (Var "R")) ")" ")" ))))) ; theorem :: HAUSDORF:35 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: HAUSDORF:36 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "holds" (Bool (Set ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: HAUSDORF:37 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q"))))) ; theorem :: HAUSDORF:38 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "R")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "R")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "Q")) "," (Set (Var "R")) ")" ")" ))))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "P", "Q" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); func :::"max_dist_min"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Real":::) means :: HAUSDORF:def 2 (Bool "ex" (Set (Var "P9")) "," (Set (Var "Q9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) "n" ")" ) ")" ) "st" (Bool "(" (Bool "P" ($#r1_hidden :::"="::: ) (Set (Var "P9"))) & (Bool "Q" ($#r1_hidden :::"="::: ) (Set (Var "Q9"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "P9")) "," (Set (Var "Q9")) ")" )) ")" )); end; :: deftheorem defines :::"max_dist_min"::: HAUSDORF:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_hausdorf :::"max_dist_min"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) "iff" (Bool "ex" (Set (Var "P9")) "," (Set (Var "Q9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "P9"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Var "Q9"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "P9")) "," (Set (Var "Q9")) ")" )) ")" )) ")" )))); definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "P", "Q" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); func :::"HausDist"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Real":::) means :: HAUSDORF:def 3 (Bool "ex" (Set (Var "P9")) "," (Set (Var "Q9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) "n" ")" ) ")" ) "st" (Bool "(" (Bool "P" ($#r1_hidden :::"="::: ) (Set (Var "P9"))) & (Bool "Q" ($#r1_hidden :::"="::: ) (Set (Var "Q9"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "P9")) "," (Set (Var "Q9")) ")" )) ")" )); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ) "st" (Bool (Bool "ex" (Set (Var "P9")) "," (Set (Var "Q9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Const "n")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "P9"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Var "Q9"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "P9")) "," (Set (Var "Q9")) ")" )) ")" ))) "holds" (Bool "ex" (Set (Var "P9")) "," (Set (Var "Q9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Const "n")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Var "P9"))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q9"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "P9")) "," (Set (Var "Q9")) ")" )) ")" )))) ; end; :: deftheorem defines :::"HausDist"::: HAUSDORF:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) "iff" (Bool "ex" (Set (Var "P9")) "," (Set (Var "Q9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "P9"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Var "Q9"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_hausdorf :::"HausDist"::: ) "(" (Set (Var "P9")) "," (Set (Var "Q9")) ")" )) ")" )) ")" )))); theorem :: HAUSDORF:39 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set ($#k3_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: HAUSDORF:40 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k3_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: HAUSDORF:41 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set ($#k3_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q"))))) ; theorem :: HAUSDORF:42 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "R")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set ($#k3_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "R")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_hausdorf :::"HausDist"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k3_hausdorf :::"HausDist"::: ) "(" (Set (Var "Q")) "," (Set (Var "R")) ")" ")" ))))) ;