:: PCOMPS_1 semantic presentation begin theorem :: PCOMPS_1:1 (Bool "for" (Set (Var "PM")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PM")) (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ))))) ; theorem :: PCOMPS_1:2 (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 ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: PCOMPS_1:3 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "FX")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set (Var "FX"))) ")" ))))) ; theorem :: PCOMPS_1:4 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k1_compts_1 :::"1TopSp"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "a"))))) ; theorem :: PCOMPS_1:5 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_compts_1 :::"1TopSp"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ; theorem :: PCOMPS_1:6 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_compts_1 :::"1TopSp"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )) "is" ($#v1_compts_1 :::"compact"::: ) )) ; theorem :: PCOMPS_1:7 (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_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_pre_topc :::"T_2"::: ) )) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); attr "IT" is :::"locally_finite"::: means :: PCOMPS_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool "{" (Set (Var "V")) where V "is" ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) "IT") & (Bool (Set (Var "V")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "W"))) ")" ) "}" "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))); end; :: deftheorem defines :::"locally_finite"::: PCOMPS_1:def 1 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool "{" (Set (Var "V")) where V "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) & (Bool (Set (Var "V")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "W"))) ")" ) "}" "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))) ")" ))); theorem :: PCOMPS_1:8 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "{" (Set (Var "V")) where V "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "FX"))) & (Bool (Set (Var "V")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "W"))) ")" ) "}" ($#r1_tarski :::"c="::: ) (Set (Var "FX")))))) ; theorem :: PCOMPS_1:9 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "," (Set (Var "GX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "FX")) ($#r1_tarski :::"c="::: ) (Set (Var "GX"))) & (Bool (Set (Var "GX")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) )) "holds" (Bool (Set (Var "FX")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) ))) ; theorem :: PCOMPS_1:10 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "FX")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Var "FX")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) ))) ; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "FX" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); func :::"clf"::: "FX" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" means :: PCOMPS_1:def 2 (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "holds" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "W")))) & (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) "FX") ")" )) ")" )); end; :: deftheorem defines :::"clf"::: PCOMPS_1:def 2 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "FX")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "FX")))) "iff" (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "W")))) & (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set (Var "FX"))) ")" )) ")" )) ")" ))); theorem :: PCOMPS_1:11 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "FX"))) "is" ($#v2_tops_2 :::"closed"::: ) ))) ; theorem :: PCOMPS_1:12 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "FX")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "FX"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: PCOMPS_1:13 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "FX")) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "V")) ($#k6_domain_1 :::"}"::: ) ))) "holds" (Bool (Set ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "FX"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "V")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: PCOMPS_1:14 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "," (Set (Var "GX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "FX")) ($#r1_tarski :::"c="::: ) (Set (Var "GX")))) "holds" (Bool (Set ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "FX"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "GX")))))) ; theorem :: PCOMPS_1:15 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "," (Set (Var "GX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_pcomps_1 :::"clf"::: ) (Set "(" (Set (Var "FX")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "GX")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "FX")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "GX")) ")" ))))) ; theorem :: PCOMPS_1:16 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "FX")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "FX")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "FX")) ")" ))))) ; theorem :: PCOMPS_1:17 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool (Set (Var "FX")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "FX")))))) ; scheme :: PCOMPS_1:sch 1 Lambda1top{ F1() -> ($#l1_pre_topc :::"TopSpace":::), F2() -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set F1 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "st" (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "Z"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "Z")) ")" )))) provided (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool (Set F4 "(" (Set (Var "Z")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) proof end; theorem :: PCOMPS_1:18 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "FX")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) )) "holds" (Bool (Set ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "FX"))) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) ))) ; theorem :: PCOMPS_1:19 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "FX"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "FX")) ")" ))))) ; theorem :: PCOMPS_1:20 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "FX")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "FX")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "FX")) ")" ))))) ; theorem :: PCOMPS_1:21 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "FX")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) ) & (Bool (Set (Var "FX")) "is" ($#v2_tops_2 :::"closed"::: ) )) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "FX"))) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; definitionlet "IT" be ($#l1_pre_topc :::"TopStruct"::: ) ; attr "IT" is :::"paracompact"::: means :: PCOMPS_1:def 3 (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "IT" "st" (Bool (Bool (Set (Var "FX")) "is" ($#m1_setfam_1 :::"Cover":::) "of" "IT") & (Bool (Set (Var "FX")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "GX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "GX")) "is" ($#v1_tops_2 :::"open"::: ) ) & (Bool (Set (Var "GX")) "is" ($#m1_setfam_1 :::"Cover":::) "of" "IT") & (Bool (Set (Var "GX")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "FX"))) & (Bool (Set (Var "GX")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) ) ")" ))); end; :: deftheorem defines :::"paracompact"::: PCOMPS_1:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_pcomps_1 :::"paracompact"::: ) ) "iff" (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "FX")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "IT"))) & (Bool (Set (Var "FX")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "GX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "GX")) "is" ($#v1_tops_2 :::"open"::: ) ) & (Bool (Set (Var "GX")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "IT"))) & (Bool (Set (Var "GX")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "FX"))) & (Bool (Set (Var "GX")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) ) ")" ))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v2_pcomps_1 :::"paracompact"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: PCOMPS_1:22 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v1_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v2_pcomps_1 :::"paracompact"::: ) )) ; theorem :: PCOMPS_1:23 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v2_pcomps_1 :::"paracompact"::: ) ) & (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "V")) "," (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "V")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "W"))) ")" )) ")" )) "holds" (Bool "ex" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "Z")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Var "Y")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Z"))) ")" )))) ; theorem :: PCOMPS_1:24 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_pre_topc :::"T_2"::: ) ) & (Bool (Set (Var "T")) "is" ($#v2_pcomps_1 :::"paracompact"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v9_pre_topc :::"regular"::: ) )) ; theorem :: PCOMPS_1:25 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_pre_topc :::"T_2"::: ) ) & (Bool (Set (Var "T")) "is" ($#v2_pcomps_1 :::"paracompact"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v10_pre_topc :::"normal"::: ) )) ; definitionlet "PM" be ($#l1_metric_1 :::"MetrStruct"::: ) ; func :::"Family_open_set"::: "PM" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "PM" means :: PCOMPS_1:def 4 (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "PM" "holds" (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "PM" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" ))) ")" )); end; :: deftheorem defines :::"Family_open_set"::: PCOMPS_1:def 4 : (Bool "for" (Set (Var "PM")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "PM")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "PM")))) "iff" (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "PM")) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PM")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" ))) ")" )) ")" ))); theorem :: PCOMPS_1:26 (Bool "for" (Set (Var "PM")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PM")) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PM")))) ")" )))) ; theorem :: PCOMPS_1:27 (Bool "for" (Set (Var "PM")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PM")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "PM")) "is" ($#v9_metric_1 :::"triangle"::: ) ) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) ")" ))))) ; theorem :: PCOMPS_1:28 (Bool "for" (Set (Var "PM")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PM")) "st" (Bool (Bool (Set (Var "PM")) "is" ($#v9_metric_1 :::"triangle"::: ) ) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ")" )))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "y")) "," (Set (Var "q")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) & (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "y")) "," (Set (Var "q")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" )) ")" ))))) ; theorem :: PCOMPS_1:29 (Bool "for" (Set (Var "PM")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PM")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "PM")) "is" ($#v9_metric_1 :::"triangle"::: ) )) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "PM"))))))) ; theorem :: PCOMPS_1:30 (Bool "for" (Set (Var "PM")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PM"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "PM"))))) ; theorem :: PCOMPS_1:31 (Bool "for" (Set (Var "PM")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "PM")) "st" (Bool (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "PM")))) & (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "PM"))))) "holds" (Bool (Set (Set (Var "V")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "W"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "PM")))))) ; theorem :: PCOMPS_1:32 (Bool "for" (Set (Var "PM")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "PM")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "PM"))))) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "PM")))))) ; theorem :: PCOMPS_1:33 (Bool "for" (Set (Var "PM")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PM"))) "," (Set "(" ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "PM")) ")" ) "#)" ) "is" ($#l1_pre_topc :::"TopSpace":::))) ; definitionlet "PM" be ($#l1_metric_1 :::"MetrStruct"::: ) ; func :::"TopSpaceMetr"::: "PM" -> ($#l1_pre_topc :::"TopStruct"::: ) equals :: PCOMPS_1:def 5 (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "PM") "," (Set "(" ($#k2_pcomps_1 :::"Family_open_set"::: ) "PM" ")" ) "#)" ); end; :: deftheorem defines :::"TopSpaceMetr"::: PCOMPS_1:def 5 : (Bool "for" (Set (Var "PM")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "PM"))) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PM"))) "," (Set "(" ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "PM")) ")" ) "#)" ))); registrationlet "PM" be ($#l1_metric_1 :::"MetrStruct"::: ) ; cluster (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "PM") -> ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ; end; registrationlet "PM" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; cluster (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "PM") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: PCOMPS_1:34 (Bool "for" (Set (Var "PM")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "PM"))) "is" ($#v8_pre_topc :::"T_2"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v8_pre_topc :::"T_2"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "D")) "," (Set (Const "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); pred "f" :::"is_metric_of"::: "D" means :: PCOMPS_1:def 6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "holds" (Bool "(" "(" (Bool (Bool (Set "f" ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "implies" (Bool (Set "f" ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & (Bool (Set "f" ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_metric_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" )) & (Bool (Set "f" ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" "f" ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" "f" ($#k1_metric_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ))) ")" )); end; :: deftheorem defines :::"is_metric_of"::: PCOMPS_1:def 6 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set (Var "D"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "f")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & (Bool (Set (Set (Var "f")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" )) & (Bool (Set (Set (Var "f")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ))) ")" )) ")" ))); theorem :: PCOMPS_1:35 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set (Var "D"))) "iff" (Bool (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set (Var "D")) "," (Set (Var "f")) "#)" ) "is" ($#l1_metric_1 :::"MetrSpace":::)) ")" ))) ; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "D")) "," (Set (Const "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); assume (Bool (Set (Const "f")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set (Const "D"))) ; func :::"SpaceMetr"::: "(" "D" "," "f" ")" -> ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrSpace":::) equals :: PCOMPS_1:def 7 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" "D" "," "f" "#)" ); end; :: deftheorem defines :::"SpaceMetr"::: PCOMPS_1:def 7 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k4_pcomps_1 :::"SpaceMetr"::: ) "(" (Set (Var "D")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set (Var "D")) "," (Set (Var "f")) "#)" )))); definitionlet "IT" be ($#l1_pre_topc :::"TopStruct"::: ) ; attr "IT" is :::"metrizable"::: means :: PCOMPS_1:def 8 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT")) & (Bool (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set "(" ($#k4_pcomps_1 :::"SpaceMetr"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "IT")) ")" )); end; :: deftheorem defines :::"metrizable"::: PCOMPS_1:def 8 : (Bool "for" (Set (Var "IT")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_pcomps_1 :::"metrizable"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT")))) & (Bool (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set "(" ($#k4_pcomps_1 :::"SpaceMetr"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "IT")))) ")" )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_pcomps_1 :::"metrizable"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: PCOMPS_1:36 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set (Var "D")))) "holds" (Bool "not" (Bool (Set ($#k4_pcomps_1 :::"SpaceMetr"::: ) "(" (Set (Var "D")) "," (Set (Var "f")) ")" ) "is" ($#v2_struct_0 :::"empty"::: ) )))) ;