:: JORDAN24 semantic presentation begin definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "a", "b" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); pred "a" "," "b" :::"realize-max-dist-in"::: "A" means :: JORDAN24:def 1 (Bool "(" (Bool "a" ($#r2_hidden :::"in"::: ) "A") & (Bool "b" ($#r2_hidden :::"in"::: ) "A") & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" "a" "," "b" ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"realize-max-dist-in"::: JORDAN24:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_topreal6 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ) ")" ) ")" )))); theorem :: JORDAN24:1 (Bool "for" (Set (Var "C")) "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 "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "C"))))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Const "M")) ")" ) "," (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Const "M")) ")" ); attr "f" is :::"isometric"::: means :: JORDAN24:def 2 (Bool "ex" (Set (Var "g")) "being" ($#v3_vectmetr :::"isometric"::: ) ($#m1_subset_1 :::"Function":::) "of" "M" "," "M" "st" (Bool (Set (Var "g")) ($#r1_funct_2 :::"="::: ) "f")); end; :: deftheorem defines :::"isometric"::: JORDAN24:def 2 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_jordan24 :::"isometric"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#v3_vectmetr :::"isometric"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "M")) "st" (Bool (Set (Var "g")) ($#r1_funct_2 :::"="::: ) (Set (Var "f")))) ")" ))); registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "M" ")" ))) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "M" ")" ))) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "M" ")" ))) ($#v1_funct_2 :::"quasi_total"::: ) ($#v2_funct_2 :::"onto"::: ) ($#v1_jordan24 :::"isometric"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "M" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "M" ")" )))))); end; registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_jordan24 :::"isometric"::: ) -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "M" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "M" ")" )))))); end; registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v2_funct_2 :::"onto"::: ) ($#v1_jordan24 :::"isometric"::: ) -> ($#v3_tops_2 :::"being_homeomorphism"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "M" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "M" ")" )))))); end; definitionlet "a" be ($#m1_subset_1 :::"Real":::); func :::"Rotate"::: "a" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) means :: JORDAN24:def 3 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set "(" (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" ) ")" ) "," "a" ")" ")" ) ")" ) "," (Set "(" ($#k4_complex1 :::"Im"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set "(" (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" ) ")" ) "," "a" ")" ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))); end; :: deftheorem defines :::"Rotate"::: JORDAN24:def 3 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "a")))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set "(" (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" ) ")" ) "," (Set (Var "a")) ")" ")" ) ")" ) "," (Set "(" ($#k4_complex1 :::"Im"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set "(" (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" ) ")" ) "," (Set (Var "a")) ")" ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))) ")" ))); theorem :: JORDAN24:2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "a"))))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_jordan24 :::"isometric"::: ) ) ")" ))) ; theorem :: JORDAN24:3 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "D")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Set "(" ($#k2_jgraph_2 :::"AffineMap"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A")) "," (Set (Var "D")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p1"))) "," (Set (Set "(" ($#k2_jgraph_2 :::"AffineMap"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A")) "," (Set (Var "D")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p2"))) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Set "(" ($#k2_jgraph_2 :::"AffineMap"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "A")) "," (Set (Var "D")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))))))) ; theorem :: JORDAN24:4 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p1"))) "," (Set (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p2"))) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "A")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))))))) ; theorem :: JORDAN24:5 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "z")) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "z")) "," (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" )))) ; theorem :: JORDAN24:6 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k1_jordan24 :::"Rotate"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k1_jordan24 :::"Rotate"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" )))) ; theorem :: JORDAN24:7 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "ex" (Set (Var "f")) "being" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Num 2)) "st" (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#r1_jordan24 :::"realize-max-dist-in"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "C")))))) ; definitionlet "T1", "T2" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T1")) "," (Set (Const "T2")); attr "f" is :::"closed"::: means :: JORDAN24:def 4 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T1" "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set "f" ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v4_pre_topc :::"closed"::: ) )); end; :: deftheorem defines :::"closed"::: JORDAN24:def 4 : (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_jordan24 :::"closed"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v4_pre_topc :::"closed"::: ) )) ")" ))); theorem :: JORDAN24:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) "iff" (Bool (Set (Var "f")) "is" ($#v2_jordan24 :::"closed"::: ) ) ")" ))) ; theorem :: JORDAN24:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" ))) ; theorem :: JORDAN24:10 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v2_connsp_1 :::"connected"::: ) )))) ; theorem :: JORDAN24:11 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_connsp_1 :::"a_component"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v3_connsp_1 :::"a_component"::: ) )))) ; theorem :: JORDAN24:12 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "T1")) ($#k1_pre_topc :::"|"::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "T2")) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ) ")" ))))) ; theorem :: JORDAN24:13 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "T1")) ($#k1_pre_topc :::"|"::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "T2")) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ))))) ; theorem :: JORDAN24:14 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "T1")) ($#k1_pre_topc :::"|"::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "T2")) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "g")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ))))) ; theorem :: JORDAN24:15 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")) "st" (Bool (Bool (Set (Var "A")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B"))))))) ; theorem :: JORDAN24:16 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "S")) "is" ($#v1_jordan1 :::"Jordan"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "S"))) "is" ($#v1_jordan1 :::"Jordan"::: ) ))) ;