:: MFOLD_1 semantic presentation begin registrationlet "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "x" "," "y" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: MFOLD_1:1 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Var "T")) "," (Set (Set (Var "T")) ($#k1_pre_topc :::"|"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" )) ($#r2_borsuk_3 :::"are_homeomorphic"::: ) )) ; theorem :: MFOLD_1:2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "b")))))) ")" ) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" ))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); attr "S" is :::"ball"::: means :: MFOLD_1:def 1 (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" )(Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "S" ($#r1_hidden :::"="::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" )))); end; :: deftheorem defines :::"ball"::: MFOLD_1:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_mfold_1 :::"ball"::: ) ) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )(Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" )))) ")" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#v4_funct_1 :::"functional"::: ) ($#v1_mfold_1 :::"ball"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ))); cluster ($#v1_mfold_1 :::"ball"::: ) -> ($#v3_pre_topc :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ))); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ($#v1_mfold_1 :::"ball"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ))); end; theorem :: MFOLD_1:3 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "ex" (Set (Var "B")) "being" ($#v1_mfold_1 :::"ball"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"Tball"::: "(" "p" "," "r" ")" -> ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) "n") equals :: MFOLD_1:def 2 (Set (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" "p" "," "r" ")" ")" )); end; :: deftheorem defines :::"Tball"::: MFOLD_1:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_mfold_1 :::"Tball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" )))))); definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"Tunit_ball"::: "n" -> ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) "n") equals :: MFOLD_1:def 3 (Set ($#k1_mfold_1 :::"Tball"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) ")" ) "," (Num 1) ")" ); end; :: deftheorem defines :::"Tunit_ball"::: MFOLD_1:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_mfold_1 :::"Tunit_ball"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mfold_1 :::"Tball"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) "," (Num 1) ")" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k2_mfold_1 :::"Tunit_ball"::: ) "n") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "s" be ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_mfold_1 :::"Tball"::: ) "(" "p" "," "s" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: MFOLD_1:4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_mfold_1 :::"Tball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ))))) ; theorem :: MFOLD_1:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Set (Var "p")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k2_mfold_1 :::"Tunit_ball"::: ) (Set (Var "n")) ")" ))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1)))) ; theorem :: MFOLD_1:6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_mfold_1 :::"Tunit_ball"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k2_mfold_1 :::"Tunit_ball"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "b")) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "b")) ($#k12_euclid :::".|"::: ) ) ")" ) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "b"))))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ))) ; theorem :: MFOLD_1:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_mfold_1 :::"Tunit_ball"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_mfold_1 :::"Tball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k2_mfold_1 :::"Tunit_ball"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p"))))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ))))) ; theorem :: MFOLD_1:8 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_mfold_1 :::"Tunit_ball"::: ) (Set (Var "n"))) "," (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n"))) ($#r2_borsuk_3 :::"are_homeomorphic"::: ) )) ; theorem :: MFOLD_1:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_mfold_1 :::"Tball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ) "," (Set ($#k1_mfold_1 :::"Tball"::: ) "(" (Set (Var "q")) "," (Set (Var "s")) ")" ) ($#r2_borsuk_3 :::"are_homeomorphic"::: ) )))) ; theorem :: MFOLD_1:10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_mfold_1 :::"ball"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Var "B")) "," (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) ($#r1_metrizts :::"are_homeomorphic"::: ) ))) ; theorem :: MFOLD_1:11 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "U")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "p")) (Bool "for" (Set (Var "B")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "U")) "," (Set (Var "B")) ($#r1_metrizts :::"are_homeomorphic"::: ) )) "holds" (Bool "ex" (Set (Var "V")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))(Bool "ex" (Set (Var "S")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "st" (Bool "(" (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "U"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) "," (Set (Var "S")) ($#r1_metrizts :::"are_homeomorphic"::: ) ) ")" ))))))) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); attr "M" is "n" :::"-locally_euclidean"::: means :: MFOLD_1:def 4 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" "M" (Bool "ex" (Set (Var "U")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "p"))(Bool "ex" (Set (Var "S")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "st" (Bool (Set (Var "U")) "," (Set (Var "S")) ($#r1_metrizts :::"are_homeomorphic"::: ) )))); end; :: deftheorem defines :::"-locally_euclidean"::: MFOLD_1:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" (Set (Var "n")) ($#v2_mfold_1 :::"-locally_euclidean"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "ex" (Set (Var "U")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "p"))(Bool "ex" (Set (Var "S")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Set (Var "U")) "," (Set (Var "S")) ($#r1_metrizts :::"are_homeomorphic"::: ) )))) ")" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k15_euclid :::"TOP-REAL"::: ) "n") -> "n" ($#v2_mfold_1 :::"-locally_euclidean"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) "n" ($#v2_mfold_1 :::"-locally_euclidean"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: MFOLD_1:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" (Set (Var "n")) ($#v2_mfold_1 :::"-locally_euclidean"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "ex" (Set (Var "U")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "p"))(Bool "ex" (Set (Var "B")) "being" ($#v1_mfold_1 :::"ball"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Set (Var "U")) "," (Set (Var "B")) ($#r1_metrizts :::"are_homeomorphic"::: ) )))) ")" ))) ; theorem :: MFOLD_1:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" (Set (Var "n")) ($#v2_mfold_1 :::"-locally_euclidean"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "ex" (Set (Var "U")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "p")) "st" (Bool (Set (Var "U")) "," (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) ($#r1_metrizts :::"are_homeomorphic"::: ) ))) ")" ))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) "n" ($#v2_mfold_1 :::"-locally_euclidean"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_frechet :::"first-countable"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_mfold_1 :::"-locally_euclidean"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tdlat_3 :::"discrete"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_tdlat_3 :::"discrete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_mfold_1 :::"-locally_euclidean"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k15_euclid :::"TOP-REAL"::: ) "n") -> ($#v5_waybel23 :::"second-countable"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v8_pre_topc :::"Hausdorff"::: ) ($#v5_waybel23 :::"second-countable"::: ) "n" ($#v2_mfold_1 :::"-locally_euclidean"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); attr "M" is "n" :::"-manifold"::: means :: MFOLD_1:def 5 (Bool "(" (Bool "M" "is" ($#v5_waybel23 :::"second-countable"::: ) ) & (Bool "M" "is" ($#v8_pre_topc :::"Hausdorff"::: ) ) & (Bool "M" "is" "n" ($#v2_mfold_1 :::"-locally_euclidean"::: ) ) ")" ); end; :: deftheorem defines :::"-manifold"::: MFOLD_1:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" (Set (Var "n")) ($#v3_mfold_1 :::"-manifold"::: ) ) "iff" (Bool "(" (Bool (Set (Var "M")) "is" ($#v5_waybel23 :::"second-countable"::: ) ) & (Bool (Set (Var "M")) "is" ($#v8_pre_topc :::"Hausdorff"::: ) ) & (Bool (Set (Var "M")) "is" (Set (Var "n")) ($#v2_mfold_1 :::"-locally_euclidean"::: ) ) ")" ) ")" ))); definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); attr "M" is :::"manifold-like"::: means :: MFOLD_1:def 6 (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "M" "is" (Set (Var "n")) ($#v3_mfold_1 :::"-manifold"::: ) )); end; :: deftheorem defines :::"manifold-like"::: MFOLD_1:def 6 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v4_mfold_1 :::"manifold-like"::: ) ) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "M")) "is" (Set (Var "n")) ($#v3_mfold_1 :::"-manifold"::: ) )) ")" )); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) "n" ($#v3_mfold_1 :::"-manifold"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) "n" ($#v3_mfold_1 :::"-manifold"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"Hausdorff"::: ) ($#v5_waybel23 :::"second-countable"::: ) "n" ($#v2_mfold_1 :::"-locally_euclidean"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v8_pre_topc :::"Hausdorff"::: ) ($#v5_waybel23 :::"second-countable"::: ) "n" ($#v2_mfold_1 :::"-locally_euclidean"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) "n" ($#v3_mfold_1 :::"-manifold"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) "n" ($#v3_mfold_1 :::"-manifold"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_mfold_1 :::"manifold-like"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v5_waybel23 :::"second-countable"::: ) ($#v1_tdlat_3 :::"discrete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v3_mfold_1 :::"-manifold"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) (Set (Const "n")) ($#v3_mfold_1 :::"-manifold"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) "n" ($#v3_mfold_1 :::"-manifold"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "M"; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v4_mfold_1 :::"manifold-like"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; definitionmode manifold is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_mfold_1 :::"manifold-like"::: ) ($#l1_pre_topc :::"TopSpace":::); end;