:: WAYBEL18 semantic presentation begin theorem :: WAYBEL18:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ")" )) "holds" (Bool (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "B")))))) ; theorem :: WAYBEL18:2 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "K")) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))) "iff" (Bool (Set (Set (Var "K")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))) ")" ))) ; definitionlet "F" be ($#m1_hidden :::"Relation":::); attr "F" is :::"TopStruct-yielding"::: means :: WAYBEL18:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "F"))) "holds" (Bool (Set (Var "x")) "is" ($#l1_pre_topc :::"TopStruct"::: ) )); end; :: deftheorem defines :::"TopStruct-yielding"::: WAYBEL18:def 1 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_waybel18 :::"TopStruct-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "x")) "is" ($#l1_pre_topc :::"TopStruct"::: ) )) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) -> ($#v2_pralg_1 :::"1-sorted-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "J" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); let "j" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "J")); :: original: :::"."::: redefine func "A" :::"."::: "j" -> ($#l1_pre_topc :::"TopStruct"::: ) ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "J" be ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func :::"product_prebasis"::: "J" -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) "J" ")" ) ")" ) means :: WAYBEL18:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) "J" ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I") & (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set "J" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) "J" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "V")) ")" ")" ))) ")" )))) ")" )); end; :: deftheorem defines :::"product_prebasis"::: WAYBEL18:def 2 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "J")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel18 :::"product_prebasis"::: ) (Set (Var "J")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "J")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set (Var "J")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "J")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "V")) ")" ")" ))) ")" )))) ")" )) ")" )))); theorem :: WAYBEL18:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "X")) "," (Set "(" ($#k1_cantor_1 :::"UniCl"::: ) (Set "(" ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set (Var "A")) ")" ) ")" ) "#)" ) "is" ($#v2_pre_topc :::"TopSpace-like"::: ) ))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "J" be ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func :::"product"::: "J" -> ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopSpace":::) means :: WAYBEL18:def 3 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) "J" ")" ))) & (Bool (Set ($#k2_waybel18 :::"product_prebasis"::: ) "J") "is" ($#m1_subset_1 :::"prebasis":::) "of" it) ")" ); end; :: deftheorem defines :::"product"::: WAYBEL18:def 3 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel18 :::"product"::: ) (Set (Var "J")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "J")) ")" ))) & (Bool (Set ($#k2_waybel18 :::"product_prebasis"::: ) (Set (Var "J"))) "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "b3"))) ")" ) ")" )))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "J" be ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k3_waybel18 :::"product"::: ) "J") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ; end; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "J" be ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); :: original: :::"."::: redefine func "J" :::"."::: "i" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "J" be ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k3_waybel18 :::"product"::: ) "J") -> ($#v1_pre_topc :::"strict"::: ) ($#v1_monoid_0 :::"constituted-Functions"::: ) ; end; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "J" be ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_waybel18 :::"product"::: ) (Set (Const "J")) ")" ); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); :: original: :::"."::: redefine func "x" :::"."::: "i" -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" "J" ($#k4_waybel18 :::"."::: ) "i" ")" ); end; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "J" be ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); func :::"proj"::: "(" "J" "," "i" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_waybel18 :::"product"::: ) "J" ")" ) "," (Set "(" "J" ($#k4_waybel18 :::"."::: ) "i" ")" ) equals :: WAYBEL18:def 4 (Set ($#k12_card_3 :::"proj"::: ) "(" (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) "J" ")" ) "," "i" ")" ); end; :: deftheorem defines :::"proj"::: WAYBEL18:def 4 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set ($#k6_waybel18 :::"proj"::: ) "(" (Set (Var "J")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_card_3 :::"proj"::: ) "(" (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "J")) ")" ) "," (Set (Var "i")) ")" ))))); theorem :: WAYBEL18:4 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "J")) ($#k4_waybel18 :::"."::: ) (Set (Var "i")) ")" ) "holds" (Bool (Set (Set "(" ($#k6_waybel18 :::"proj"::: ) "(" (Set (Var "J")) "," (Set (Var "i")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "J")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "P")) ")" ")" ))))))) ; theorem :: WAYBEL18:5 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set ($#k6_waybel18 :::"proj"::: ) "(" (Set (Var "J")) "," (Set (Var "i")) ")" ) "is" ($#v5_pre_topc :::"continuous"::: ) )))) ; theorem :: WAYBEL18:6 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k3_waybel18 :::"product"::: ) (Set (Var "J")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" ($#k6_waybel18 :::"proj"::: ) "(" (Set (Var "J")) "," (Set (Var "i")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#v5_pre_topc :::"continuous"::: ) )) ")" ))))) ; begin definitionlet "Z" be ($#l1_pre_topc :::"TopStruct"::: ) ; attr "Z" is :::"injective"::: means :: WAYBEL18:def 5 (Bool "for" (Set (Var "X")) "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 "X")) "," "Z" "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," "Z" "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))))); end; :: deftheorem defines :::"injective"::: WAYBEL18:def 5 : (Bool "for" (Set (Var "Z")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "Z")) "is" ($#v2_waybel18 :::"injective"::: ) ) "iff" (Bool "for" (Set (Var "X")) "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 "X")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))))) ")" )); theorem :: WAYBEL18:7 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_waybel18 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "J")) ($#k4_waybel18 :::"."::: ) (Set (Var "i"))) "is" ($#v2_waybel18 :::"injective"::: ) ) ")" )) "holds" (Bool (Set ($#k3_waybel18 :::"product"::: ) (Set (Var "J"))) "is" ($#v2_waybel18 :::"injective"::: ) ))) ; theorem :: WAYBEL18:8 (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" ($#v2_waybel18 :::"injective"::: ) )) "holds" (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) ($#r1_borsuk_1 :::"is_a_retract_of"::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "S")) "is" ($#v2_waybel18 :::"injective"::: ) ))) ; definitionlet "X" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); func :::"Image"::: "f" -> ($#m1_pre_topc :::"SubSpace"::: ) "of" "Y" equals :: WAYBEL18:def 6 (Set "Y" ($#k1_pre_topc :::"|"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) "f" ")" )); end; :: deftheorem defines :::"Image"::: WAYBEL18:def 6 : (Bool "for" (Set (Var "X")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k7_waybel18 :::"Image"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y")) ($#k1_pre_topc :::"|"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" )))))); registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set ($#k7_waybel18 :::"Image"::: ) "f") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: WAYBEL18:9 (Bool "for" (Set (Var "X")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_waybel18 :::"Image"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))))))) ; definitionlet "X" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); func :::"corestr"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set "(" ($#k7_waybel18 :::"Image"::: ) "f" ")" ) equals :: WAYBEL18:def 7 "f"; end; :: deftheorem defines :::"corestr"::: WAYBEL18:def 7 : (Bool "for" (Set (Var "X")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "Y")) "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 "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k8_waybel18 :::"corestr"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))))); theorem :: WAYBEL18:10 (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" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set ($#k8_waybel18 :::"corestr"::: ) (Set (Var "f"))) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; registrationlet "X" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set ($#k8_waybel18 :::"corestr"::: ) "f") -> ($#v2_funct_2 :::"onto"::: ) ; end; definitionlet "X", "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; pred "X" :::"is_Retract_of"::: "Y" means :: WAYBEL18:def 8 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" "Y" "," "Y" "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k7_waybel18 :::"Image"::: ) (Set (Var "f"))) "," "X" ($#r1_t_0topsp :::"are_homeomorphic"::: ) ) ")" )); end; :: deftheorem defines :::"is_Retract_of"::: WAYBEL18:def 8 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_waybel18 :::"is_Retract_of"::: ) (Set (Var "Y"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k7_waybel18 :::"Image"::: ) (Set (Var "f"))) "," (Set (Var "X")) ($#r1_t_0topsp :::"are_homeomorphic"::: ) ) ")" )) ")" )); theorem :: WAYBEL18:11 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v2_waybel18 :::"injective"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set ($#k8_waybel18 :::"corestr"::: ) (Set (Var "f"))) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )) "holds" (Bool (Set (Var "T")) ($#r1_waybel18 :::"is_Retract_of"::: ) (Set (Var "S"))))) ; definitionfunc :::"Sierpinski_Space"::: -> ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopStruct"::: ) means :: WAYBEL18:def 9 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) )) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) ($#k1_enumset1 :::"}"::: ) )) ")" ); end; :: deftheorem defines :::"Sierpinski_Space"::: WAYBEL18:def 9 : (Bool "for" (Set (Var "b1")) "being" ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) )) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) ($#k1_enumset1 :::"}"::: ) )) ")" ) ")" )); registration cluster (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ; end; registration cluster (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) -> ($#v1_pre_topc :::"strict"::: ) ($#v6_pre_topc :::"T_0"::: ) ; end; registration cluster (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) -> ($#v1_pre_topc :::"strict"::: ) ($#v2_waybel18 :::"injective"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set "I" ($#k2_funcop_1 :::"-->"::: ) "S") -> ($#v4_waybel_3 :::"non-Empty"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set "I" ($#k2_funcop_1 :::"-->"::: ) "T") -> ($#v1_waybel18 :::"TopStruct-yielding"::: ) ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k5_yellow_1 :::"product"::: ) (Set "(" "I" ($#k7_funcop_1 :::"-->"::: ) "L" ")" )) -> ($#v5_orders_2 :::"antisymmetric"::: ) ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k5_yellow_1 :::"product"::: ) (Set "(" "I" ($#k7_funcop_1 :::"-->"::: ) "L" ")" )) -> ($#v4_orders_2 :::"transitive"::: ) ; end; theorem :: WAYBEL18:12 (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set ($#k3_yellow_1 :::"BoolePoset"::: ) (Num 1)) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) )))) ; theorem :: WAYBEL18:13 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "{" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set "(" (Set (Var "I")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ")" ")" ) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) : (Bool verum) "}" "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set "(" ($#k3_waybel18 :::"product"::: ) (Set "(" (Set (Var "I")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" ) ")" ))) ; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set ($#k5_yellow_1 :::"product"::: ) (Set "(" "I" ($#k7_funcop_1 :::"-->"::: ) "L" ")" )) -> ($#v1_lattice3 :::"with_suprema"::: ) ($#v3_lattice3 :::"complete"::: ) ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_waybel_8 :::"algebraic"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set ($#k5_yellow_1 :::"product"::: ) (Set "(" "I" ($#k7_funcop_1 :::"-->"::: ) "X" ")" )) -> ($#v2_waybel_8 :::"algebraic"::: ) ; end; theorem :: WAYBEL18:14 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k5_yellow_1 :::"product"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Num 1) ")" ) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) & (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_funct_3 :::"chi"::: ) "(" (Set (Var "Y")) "," (Set (Var "X")) ")" )) ")" ) ")" ))) ; theorem :: WAYBEL18:15 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set ($#k5_yellow_1 :::"product"::: ) (Set "(" (Set (Var "I")) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Num 1) ")" ) ")" )) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k3_waybel18 :::"product"::: ) (Set "(" (Set (Var "I")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" ) ")" ))))) ; theorem :: WAYBEL18:16 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "T")) "is" ($#v2_waybel18 :::"injective"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v2_waybel18 :::"injective"::: ) )) ; theorem :: WAYBEL18:17 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set ($#k5_yellow_1 :::"product"::: ) (Set "(" (Set (Var "I")) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Num 1) ")" ) ")" )) "holds" (Bool (Set (Var "T")) "is" ($#v2_waybel18 :::"injective"::: ) ))) ; theorem :: WAYBEL18:18 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"T_0-TopSpace":::) (Bool "ex" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set "(" ($#k3_waybel18 :::"product"::: ) (Set "(" (Set (Var "M")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" ) ")" ) "st" (Bool (Set ($#k8_waybel18 :::"corestr"::: ) (Set (Var "f"))) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )))) ; theorem :: WAYBEL18:19 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"T_0-TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v2_waybel18 :::"injective"::: ) )) "holds" (Bool "ex" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "T")) ($#r1_waybel18 :::"is_Retract_of"::: ) (Set ($#k3_waybel18 :::"product"::: ) (Set "(" (Set (Var "M")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" ))))) ;