:: COMPTS_1 semantic presentation begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; attr "T" is :::"compact"::: means :: COMPTS_1:def 1 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "T" "st" (Bool (Bool (Set (Var "F")) "is" ($#m1_setfam_1 :::"Cover":::) "of" "T") & (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "G")) "is" ($#m1_setfam_1 :::"Cover":::) "of" "T") & (Bool (Set (Var "G")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))); end; :: deftheorem defines :::"compact"::: COMPTS_1:def 1 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_compts_1 :::"compact"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) & (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "G")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) & (Bool (Set (Var "G")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))) ")" )); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); redefine attr "T" is :::"regular"::: means :: COMPTS_1:def 2 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool "ex" (Set (Var "W")) "," (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Var "W")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "V"))) ")" )))); redefine attr "T" is :::"normal"::: means :: COMPTS_1:def 3 (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "W")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "V")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "W")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "V")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "W")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "V")))) "holds" (Bool "ex" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "W")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set (Var "P")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Q"))) ")" ))); end; :: deftheorem defines :::"regular"::: COMPTS_1:def 2 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v9_pre_topc :::"regular"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool "ex" (Set (Var "W")) "," (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Var "W")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "V"))) ")" )))) ")" )); :: deftheorem defines :::"normal"::: COMPTS_1:def 3 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v10_pre_topc :::"normal"::: ) ) "iff" (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "W")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "V")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "W")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "V")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "W")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "V")))) "holds" (Bool "ex" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "W")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set (Var "P")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Q"))) ")" ))) ")" )); notationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; synonym :::"Hausdorff"::: "T" for :::"T_2"::: ; end; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); attr "P" is :::"compact"::: means :: COMPTS_1:def 4 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "T" "st" (Bool (Bool (Set (Var "F")) "is" ($#m1_setfam_1 :::"Cover"::: ) "of" "P") & (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "G")) "is" ($#m1_setfam_1 :::"Cover"::: ) "of" "P") & (Bool (Set (Var "G")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))); end; :: deftheorem defines :::"compact"::: COMPTS_1:def 4 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#m1_setfam_1 :::"Cover"::: ) "of" (Set (Var "P"))) & (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "G")) "is" ($#m1_setfam_1 :::"Cover"::: ) "of" (Set (Var "P"))) & (Bool (Set (Var "G")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))) ")" ))); registrationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v2_compts_1 :::"compact"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: COMPTS_1:1 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_compts_1 :::"compact"::: ) ) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T"))) "is" ($#v2_compts_1 :::"compact"::: ) ) ")" )) ; theorem :: COMPTS_1:2 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) ) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q")))) "holds" (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) ")" )))) ; theorem :: COMPTS_1:3 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) "iff" (Bool (Set (Set (Var "T")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P"))) "is" ($#v1_compts_1 :::"compact"::: ) ) ")" ) ")" & "(" (Bool (Bool (Set (Var "T")) "is" ($#v2_pre_topc :::"TopSpace-like"::: ) ) & (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) "iff" (Bool (Set (Set (Var "T")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P"))) "is" ($#v1_compts_1 :::"compact"::: ) ) ")" ) ")" ")" ))) ; theorem :: COMPTS_1:4 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_compts_1 :::"compact"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_finset_1 :::"centered"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) )) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" )) ; theorem :: COMPTS_1:5 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_compts_1 :::"compact"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) ) & (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "G")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ")" )) ; theorem :: COMPTS_1:6 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v8_pre_topc :::"T_2"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool "ex" (Set (Var "PS")) "," (Set (Var "QS")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool "(" (Bool (Set (Var "PS")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "QS")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "PS"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "QS"))) & (Bool (Set (Var "PS")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "QS"))) ")" ))))) ; theorem :: COMPTS_1:7 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "PS")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v8_pre_topc :::"T_2"::: ) ) & (Bool (Set (Var "PS")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Var "PS")) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: COMPTS_1:8 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v1_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ))) ; theorem :: COMPTS_1:9 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "PS")) "," (Set (Var "QS")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "PS")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "QS")) ($#r1_tarski :::"c="::: ) (Set (Var "PS"))) & (Bool (Set (Var "QS")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "QS")) "is" ($#v2_compts_1 :::"compact"::: ) ))) ; theorem :: COMPTS_1:10 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Q"))) "is" ($#v2_compts_1 :::"compact"::: ) ))) ; theorem :: COMPTS_1:11 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "PS")) "," (Set (Var "QS")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v8_pre_topc :::"T_2"::: ) ) & (Bool (Set (Var "PS")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "QS")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Set (Var "PS")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "QS"))) "is" ($#v2_compts_1 :::"compact"::: ) ))) ; theorem :: COMPTS_1:12 (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v8_pre_topc :::"T_2"::: ) ) & (Bool (Set (Var "TS")) "is" ($#v1_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Var "TS")) "is" ($#v9_pre_topc :::"regular"::: ) )) ; theorem :: COMPTS_1:13 (Bool "for" (Set (Var "TS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v8_pre_topc :::"T_2"::: ) ) & (Bool (Set (Var "TS")) "is" ($#v1_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Var "TS")) "is" ($#v10_pre_topc :::"normal"::: ) )) ; theorem :: COMPTS_1:14 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v1_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "S")) "is" ($#v1_compts_1 :::"compact"::: ) )))) ; theorem :: COMPTS_1:15 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))) "is" ($#v2_compts_1 :::"compact"::: ) ))))) ; theorem :: COMPTS_1:16 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "SS")) "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 "TS")) "," (Set (Var "SS")) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v1_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "SS")) "is" ($#v8_pre_topc :::"T_2"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "SS")))) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "for" (Set (Var "PS")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "PS")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "PS"))) "is" ($#v4_pre_topc :::"closed"::: ) ))))) ; theorem :: COMPTS_1:17 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "SS")) "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 "TS")) "," (Set (Var "SS")) "st" (Bool (Bool (Set (Var "TS")) "is" ($#v1_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "SS")) "is" ($#v8_pre_topc :::"T_2"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "TS")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "SS")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )))) ; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"1TopSp"::: "D" -> ($#l1_pre_topc :::"TopStruct"::: ) equals :: COMPTS_1:def 5 (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" "D" "," (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) "D" ")" ) ")" ) "#)" ); end; :: deftheorem defines :::"1TopSp"::: COMPTS_1:def 5 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_compts_1 :::"1TopSp"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "D")) "," (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "D")) ")" ) ")" ) "#)" ))); registrationlet "D" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_compts_1 :::"1TopSp"::: ) "D") -> ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_compts_1 :::"1TopSp"::: ) "D") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_compts_1 :::"1TopSp"::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) )) -> ($#v8_pre_topc :::"T_2"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v8_pre_topc :::"T_2"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"T_2"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v2_compts_1 :::"compact"::: ) -> ($#v4_pre_topc :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registrationlet "A" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_compts_1 :::"1TopSp"::: ) "A") -> ($#v8_struct_0 :::"finite"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registration cluster ($#v8_struct_0 :::"finite"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) -> ($#v1_compts_1 :::"compact"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: COMPTS_1:18 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v1_compts_1 :::"compact"::: ) )) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_finset_1 :::"finite"::: ) -> ($#v2_compts_1 :::"compact"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registration cluster ($#v2_struct_0 :::"empty"::: ) -> ($#v8_pre_topc :::"T_2"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "T" be ($#v8_pre_topc :::"T_2"::: ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster -> ($#v8_pre_topc :::"T_2"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "T"; end; theorem :: COMPTS_1:19 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_compts_1 :::"compact"::: ) ) "iff" (Bool (Set (Var "B")) "is" ($#v2_compts_1 :::"compact"::: ) ) ")" ))))) ; theorem :: COMPTS_1:20 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "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 "T")) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "S")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T2")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) & (Bool (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Var "T1")) "is" ($#v1_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "T2")) "is" ($#v1_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "T")) "is" ($#v8_pre_topc :::"T_2"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")))))))) ; theorem :: COMPTS_1:21 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "S")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T2")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) & (Bool (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set (Var "T1")) "is" ($#v1_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "T2")) "is" ($#v1_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "T")) "is" ($#v8_pre_topc :::"T_2"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "p1")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "p2"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")))))))) ; begin registrationlet "S" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "S") -> ($#v1_tops_2 :::"open"::: ) ; end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_tops_2 :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" )); end; theorem :: COMPTS_1:22 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))) "iff" (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" )) ")" ))) ; theorem :: COMPTS_1:23 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))) "iff" (Bool (Set (Var "X")) "is" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" )) ")" ))) ;