:: JORDAN1K semantic presentation begin theorem :: JORDAN1K:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )))))) ; theorem :: JORDAN1K:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))))) ; theorem :: JORDAN1K:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ))))))) ; theorem :: JORDAN1K:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ) ($#k3_subset_1 :::"`"::: ) )))))) ; theorem :: JORDAN1K:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ))))))) ; begin theorem :: JORDAN1K:6 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "T")))) "iff" (Bool (Set (Var "A")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ))) ; theorem :: JORDAN1K:7 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: JORDAN1K:8 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v6_tbsp_1 :::"bounded"::: ) )) "holds" (Bool "not" (Bool (Set (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v6_tbsp_1 :::"bounded"::: ) )))) ; theorem :: JORDAN1K:9 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "C")) "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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "holds" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: JORDAN1K:10 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "C")) "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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) ")" )) "holds" (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "C")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))))))) ; theorem :: JORDAN1K:11 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "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 ($#k7_weierstr :::"min_dist_min"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: JORDAN1K:12 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k7_weierstr :::"min_dist_min"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: JORDAN1K:13 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "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 "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) ")" )) "holds" (Bool (Set ($#k7_weierstr :::"min_dist_min"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r")))))) ; begin theorem :: JORDAN1K:14 (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")) ")" ) "holds" (Bool "(" "not" (Bool (Set (Var "P")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Set (Var "Q")) ($#k3_subset_1 :::"`"::: ) )) "or" (Bool (Set (Var "P")) ($#r1_jordan2c :::"is_inside_component_of"::: ) (Set (Var "Q"))) "or" (Bool (Set (Var "P")) ($#r2_jordan2c :::"is_outside_component_of"::: ) (Set (Var "Q"))) ")" ))) ; theorem :: JORDAN1K:15 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k1_jordan2c :::"BDD"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))) ; theorem :: JORDAN1K:16 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_jordan2c :::"BDD"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))) ; theorem :: JORDAN1K:17 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k2_jordan2c :::"UBD"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))) ; theorem :: JORDAN1K:18 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_jordan2c :::"UBD"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))) ; theorem :: JORDAN1K:19 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" "not" (Bool (Set (Var "P")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Q"))) "or" (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "Q")))) "or" (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set ($#k1_jordan2c :::"BDD"::: ) (Set (Var "Q")))) ")" )))) ; begin theorem :: JORDAN1K:20 (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_topreal6 :::"dist"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "q")) ")" ")" ))))) ; theorem :: JORDAN1K:21 (Bool "for" (Set (Var "q1")) "," (Set (Var "q")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set "(" (Set (Var "q1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "q2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ))) ; theorem :: JORDAN1K:22 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: JORDAN1K:23 (Bool "for" (Set (Var "q1")) "," (Set (Var "q")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set "(" (Set (Var "q1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "q2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ))) ; theorem :: JORDAN1K:24 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ")" ))) ; theorem :: JORDAN1K:25 (Bool "for" (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set "(" (Set (Var "q")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q1")) ")" ) "," (Set "(" (Set (Var "q")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q2")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ))) ; theorem :: JORDAN1K:26 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ))))) ; theorem :: JORDAN1K:27 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ))))) ; theorem :: JORDAN1K:28 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "q")) "," (Set "(" (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ))))) ; theorem :: JORDAN1K:29 (Bool "for" (Set (Var "p")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ))) "holds" (Bool (Set (Set "(" ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "q1")) "," (Set (Var "p")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ))) ; theorem :: JORDAN1K:30 (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q2")) "," (Set (Var "p")) ")" )) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2")))) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "q1")) "," (Set (Var "p")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "q2")) "," (Set (Var "p")) ")" ))) ; theorem :: JORDAN1K:31 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ))) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "y")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" ))) ; begin theorem :: JORDAN1K:32 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k2_jgraph_2 :::"AffineMap"::: ) "(" (Set (Var "r")) "," (Set (Var "s1")) "," (Set (Var "r")) "," (Set (Var "s2")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "s1")) "," (Set (Var "s2")) ($#k19_euclid :::"]|"::: ) ))))) ; theorem :: JORDAN1K:33 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k2_jgraph_2 :::"AffineMap"::: ) "(" (Set (Var "r")) "," (Set "(" (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set (Var "r")) "," (Set "(" (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q")))))) ; theorem :: JORDAN1K:34 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "s2")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k2_jgraph_2 :::"AffineMap"::: ) "(" (Set (Var "s1")) "," (Set (Var "t1")) "," (Set (Var "s2")) "," (Set (Var "t2")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k2_jgraph_2 :::"AffineMap"::: ) "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "s1")) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "t1")) ($#k10_real_1 :::"/"::: ) (Set (Var "s1")) ")" ) ")" ) "," (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "s2")) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "t2")) ($#k10_real_1 :::"/"::: ) (Set (Var "s2")) ")" ) ")" ) ")" ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" )))) ; theorem :: JORDAN1K:35 (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k2_jgraph_2 :::"AffineMap"::: ) "(" (Set (Var "r")) "," (Set "(" (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set (Var "r")) "," (Set "(" (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "y")) "," (Num 1) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: JORDAN1K:36 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "C")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k2_jgraph_2 :::"AffineMap"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ")" ) "is" ($#v2_funct_2 :::"onto"::: ) )) ; theorem :: JORDAN1K:37 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v2_connsp_1 :::"connected"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )))) ; begin definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); func :::"dist_min"::: "(" "A" "," "B" ")" -> ($#m1_subset_1 :::"Real":::) means :: JORDAN1K:def 1 (Bool "ex" (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) "n" ")" ) ")" ) "st" (Bool "(" (Bool "A" ($#r1_hidden :::"="::: ) (Set (Var "A9"))) & (Bool "B" ($#r1_hidden :::"="::: ) (Set (Var "B9"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k7_weierstr :::"min_dist_min"::: ) "(" (Set (Var "A9")) "," (Set (Var "B9")) ")" )) ")" )); end; :: deftheorem defines :::"dist_min"::: JORDAN1K:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "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 ($#k1_jordan1k :::"dist_min"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool "ex" (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A9"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "B9"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_weierstr :::"min_dist_min"::: ) "(" (Set (Var "A9")) "," (Set (Var "B9")) ")" )) ")" )) ")" )))); definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "P", "Q" 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")) ")" ); :: original: :::"min_dist_min"::: redefine func :::"min_dist_min"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); commutativity (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~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")) ")" ) "holds" (Bool (Set ($#k7_weierstr :::"min_dist_min"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_weierstr :::"min_dist_min"::: ) "(" (Set (Var "Q")) "," (Set (Var "P")) ")" ))) ; :: original: :::"max_dist_max"::: redefine func :::"max_dist_max"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); commutativity (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~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")) ")" ) "holds" (Bool (Set ($#k10_weierstr :::"max_dist_max"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_weierstr :::"max_dist_max"::: ) "(" (Set (Var "Q")) "," (Set (Var "P")) ")" ))) ; end; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); :: original: :::"dist_min"::: redefine func :::"dist_min"::: "(" "A" "," "B" ")" -> ($#m1_subset_1 :::"Real":::); commutativity (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ) "holds" (Bool (Set ($#k1_jordan1k :::"dist_min"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan1k :::"dist_min"::: ) "(" (Set (Var "B")) "," (Set (Var "A")) ")" ))) ; end; theorem :: JORDAN1K:38 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "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 ($#k1_jordan1k :::"dist_min"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: JORDAN1K:39 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_jordan1k :::"dist_min"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: JORDAN1K:40 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "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 "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) ")" )) "holds" (Bool (Set ($#k1_jordan1k :::"dist_min"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r")))))) ; theorem :: JORDAN1K:41 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "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 "C")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k1_jordan1k :::"dist_min"::: ) "(" (Set (Var "A")) "," (Set (Var "D")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_jordan1k :::"dist_min"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ))))) ; theorem :: JORDAN1K:42 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set ($#k4_jordan1k :::"dist_min"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) ")" )))) ; theorem :: JORDAN1K:43 (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 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k4_jordan1k :::"dist_min"::: ) "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) "," (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "q")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); func :::"dist"::: "(" "p" "," "B" ")" -> ($#m1_subset_1 :::"Real":::) equals :: JORDAN1K:def 2 (Set ($#k1_jordan1k :::"dist_min"::: ) "(" (Set ($#k6_domain_1 :::"{"::: ) "p" ($#k6_domain_1 :::"}"::: ) ) "," "B" ")" ); end; :: deftheorem defines :::"dist"::: JORDAN1K:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k5_jordan1k :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan1k :::"dist_min"::: ) "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) "," (Set (Var "B")) ")" ))))); theorem :: JORDAN1K:44 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k5_jordan1k :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: JORDAN1K:45 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k5_jordan1k :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: JORDAN1K:46 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k5_jordan1k :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) ")" ))))) ; theorem :: JORDAN1K:47 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k5_jordan1k :::"dist"::: ) "(" (Set (Var "q")) "," (Set (Var "D")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_jordan1k :::"dist"::: ) "(" (Set (Var "q")) "," (Set (Var "C")) ")" )))))) ; theorem :: JORDAN1K:48 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) ")" )) "holds" (Bool (Set ($#k5_jordan1k :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))))))) ; theorem :: JORDAN1K:49 (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 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k5_jordan1k :::"dist"::: ) "(" (Set (Var "p")) "," (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "q")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )))) ; theorem :: JORDAN1K:50 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k5_jordan1k :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))))) ; theorem :: JORDAN1K:51 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "B")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k5_jordan1k :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "B")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_jordan1k :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "A")) ")" ))))) ;