:: NAGATA_1 semantic presentation begin definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); attr "F" is :::"discrete"::: means :: NAGATA_1:def 1 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" (Bool "ex" (Set (Var "O")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set (Var "O")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A"))) & (Bool (Set (Var "O")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" ) ")" ))); end; :: deftheorem defines :::"discrete"::: NAGATA_1:def 1 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_nagata_1 :::"discrete"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "O")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "O")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A"))) & (Bool (Set (Var "O")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" ) ")" ))) ")" ))); registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_nagata_1 :::"discrete"::: ) 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; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_nagata_1 :::"discrete"::: ) 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 :: NAGATA_1:1 (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_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "A")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool (Set (Var "F")) "is" ($#v1_nagata_1 :::"discrete"::: ) ))) ; theorem :: NAGATA_1:2 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) "is" ($#v1_nagata_1 :::"discrete"::: ) )) "holds" (Bool (Set (Var "F")) "is" ($#v1_nagata_1 :::"discrete"::: ) ))) ; theorem :: NAGATA_1:3 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_nagata_1 :::"discrete"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "G"))) "is" ($#v1_nagata_1 :::"discrete"::: ) ))) ; theorem :: NAGATA_1:4 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_nagata_1 :::"discrete"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k7_subset_1 :::"\"::: ) (Set (Var "G"))) "is" ($#v1_nagata_1 :::"discrete"::: ) ))) ; theorem :: NAGATA_1:5 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_nagata_1 :::"discrete"::: ) ) & (Bool (Set (Var "G")) "is" ($#v1_nagata_1 :::"discrete"::: ) ) & (Bool (Set ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "F")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "H")) "is" ($#v1_nagata_1 :::"discrete"::: ) ))) ; theorem :: NAGATA_1:6 (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_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_nagata_1 :::"discrete"::: ) ) & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Bool "not" (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))))) ; theorem :: NAGATA_1:7 (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_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_nagata_1 :::"discrete"::: ) )) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "O")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) & (Bool (Set (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "O")) ($#k6_domain_1 :::"}"::: ) ) "," (Set (Var "F")) ")" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ) ")" ))))) ; theorem :: NAGATA_1:8 (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_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_nagata_1 :::"discrete"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "O")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) & (Bool (Set (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "O")) ($#k6_domain_1 :::"}"::: ) ) "," (Set (Var "F")) ")" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Bool "not" (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) ")" ) ")" ) ")" ))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "F" be ($#v1_nagata_1 :::"discrete"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); cluster (Set ($#k1_pcomps_1 :::"clf"::: ) "F") -> ($#v1_nagata_1 :::"discrete"::: ) ; end; theorem :: NAGATA_1:9 (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_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_nagata_1 :::"discrete"::: ) )) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")) ")" )))))) ; theorem :: NAGATA_1:10 (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_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_nagata_1 :::"discrete"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "F")) ")" ))))) ; theorem :: NAGATA_1:11 (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_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_nagata_1 :::"discrete"::: ) )) "holds" (Bool (Set (Var "F")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) ))) ; definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); mode FamilySequence of "T" is ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) ")" ); end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "Un" be ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Const "T")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"."::: redefine func "Un" :::"."::: "n" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T"; end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "Un" be ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Const "T")); :: original: :::"Union"::: redefine func :::"Union"::: "Un" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T"; end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "Un" be ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Const "T")); attr "Un" is :::"sigma_discrete"::: means :: NAGATA_1:def 2 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "Un" ($#k1_nagata_1 :::"."::: ) (Set (Var "n"))) "is" ($#v1_nagata_1 :::"discrete"::: ) )); end; :: deftheorem defines :::"sigma_discrete"::: NAGATA_1:def 2 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Un")) "being" ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "Un")) "is" ($#v2_nagata_1 :::"sigma_discrete"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "Un")) ($#k1_nagata_1 :::"."::: ) (Set (Var "n"))) "is" ($#v1_nagata_1 :::"discrete"::: ) )) ")" ))); registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v1_funct_2 :::"quasi_total"::: ) ($#v2_nagata_1 :::"sigma_discrete"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "Un" be ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Const "T")); attr "Un" is :::"sigma_locally_finite"::: means :: NAGATA_1:def 3 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "Un" ($#k1_nagata_1 :::"."::: ) (Set (Var "n"))) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) )); end; :: deftheorem defines :::"sigma_locally_finite"::: NAGATA_1:def 3 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Un")) "being" ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "Un")) "is" ($#v3_nagata_1 :::"sigma_locally_finite"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "Un")) ($#k1_nagata_1 :::"."::: ) (Set (Var "n"))) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) )) ")" ))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); attr "F" is :::"sigma_discrete"::: means :: NAGATA_1:def 4 (Bool "ex" (Set (Var "f")) "being" ($#v2_nagata_1 :::"sigma_discrete"::: ) ($#m1_subset_1 :::"FamilySequence":::) "of" "T" "st" (Bool "F" ($#r1_hidden :::"="::: ) (Set ($#k2_nagata_1 :::"Union"::: ) (Set (Var "f"))))); end; :: deftheorem defines :::"sigma_discrete"::: NAGATA_1:def 4 : (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_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_nagata_1 :::"sigma_discrete"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#v2_nagata_1 :::"sigma_discrete"::: ) ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k2_nagata_1 :::"Union"::: ) (Set (Var "f"))))) ")" ))); notationlet "X" be ($#m1_hidden :::"set"::: ) ; antonym :::"uncountable"::: "X" for :::"countable"::: ; end; registration cluster ($#v4_card_3 :::"uncountable"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v1_funct_2 :::"quasi_total"::: ) ($#v3_nagata_1 :::"sigma_locally_finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: NAGATA_1:12 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Un")) "being" ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Un")) "is" ($#v2_nagata_1 :::"sigma_discrete"::: ) )) "holds" (Bool (Set (Var "Un")) "is" ($#v3_nagata_1 :::"sigma_locally_finite"::: ) ))) ; theorem :: NAGATA_1:13 (Bool "for" (Set (Var "A")) "being" ($#v4_card_3 :::"uncountable"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k1_compts_1 :::"1TopSp"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) ) & (Bool (Bool "not" (Set (Var "F")) "is" ($#v4_nagata_1 :::"sigma_discrete"::: ) )) ")" ))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "Un" be ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Const "T")); attr "Un" is :::"Basis_sigma_discrete"::: means :: NAGATA_1:def 5 (Bool "(" (Bool "Un" "is" ($#v2_nagata_1 :::"sigma_discrete"::: ) ) & (Bool (Set ($#k2_nagata_1 :::"Union"::: ) "Un") "is" ($#m1_subset_1 :::"Basis":::) "of" "T") ")" ); end; :: deftheorem defines :::"Basis_sigma_discrete"::: NAGATA_1:def 5 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Un")) "being" ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "Un")) "is" ($#v5_nagata_1 :::"Basis_sigma_discrete"::: ) ) "iff" (Bool "(" (Bool (Set (Var "Un")) "is" ($#v2_nagata_1 :::"sigma_discrete"::: ) ) & (Bool (Set ($#k2_nagata_1 :::"Union"::: ) (Set (Var "Un"))) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))) ")" ) ")" ))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "Un" be ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Const "T")); attr "Un" is :::"Basis_sigma_locally_finite"::: means :: NAGATA_1:def 6 (Bool "(" (Bool "Un" "is" ($#v3_nagata_1 :::"sigma_locally_finite"::: ) ) & (Bool (Set ($#k2_nagata_1 :::"Union"::: ) "Un") "is" ($#m1_subset_1 :::"Basis":::) "of" "T") ")" ); end; :: deftheorem defines :::"Basis_sigma_locally_finite"::: NAGATA_1:def 6 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Un")) "being" ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "Un")) "is" ($#v6_nagata_1 :::"Basis_sigma_locally_finite"::: ) ) "iff" (Bool "(" (Bool (Set (Var "Un")) "is" ($#v3_nagata_1 :::"sigma_locally_finite"::: ) ) & (Bool (Set ($#k2_nagata_1 :::"Union"::: ) (Set (Var "Un"))) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))) ")" ) ")" ))); theorem :: NAGATA_1:14 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "PM")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PM")) "holds" (Bool (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "PM")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k10_metric_1 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "PM"))))))) ; theorem :: NAGATA_1:15 (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" ($#v3_pcomps_1 :::"metrizable"::: ) )) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v9_pre_topc :::"regular"::: ) ) & (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) ) ")" )) ; theorem :: NAGATA_1:16 (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" ($#v3_pcomps_1 :::"metrizable"::: ) )) "holds" (Bool "ex" (Set (Var "Un")) "being" ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "Un")) "is" ($#v6_nagata_1 :::"Basis_sigma_locally_finite"::: ) ))) ; theorem :: NAGATA_1:17 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "U")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )) "holds" (Bool (Set ($#k1_prob_1 :::"Union"::: ) (Set (Var "U"))) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: NAGATA_1:18 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "U")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "U")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "U")))) "holds" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set (Var "W")))) & (Bool (Set ($#k1_prob_1 :::"Union"::: ) (Set (Var "W"))) ($#r1_tarski :::"c="::: ) (Set (Var "U"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "W")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "U"))) & (Bool (Set (Set (Var "W")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Var "T")) "is" ($#v10_pre_topc :::"normal"::: ) )) ; theorem :: NAGATA_1:19 (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" ($#v9_pre_topc :::"regular"::: ) )) "holds" (Bool "for" (Set (Var "Bn")) "being" ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k2_nagata_1 :::"Union"::: ) (Set (Var "Bn"))) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")))) "holds" (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "U")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "U")))) "holds" (Bool "ex" (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "O"))) ($#r1_tarski :::"c="::: ) (Set (Var "U"))) & (Bool (Set (Var "O")) ($#r2_hidden :::"in"::: ) (Set ($#k2_nagata_1 :::"Union"::: ) (Set (Var "Bn")))) ")" )))))) ; theorem :: NAGATA_1:20 (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" ($#v9_pre_topc :::"regular"::: ) ) & (Bool "ex" (Set (Var "Bn")) "being" ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "Bn")) "is" ($#v6_nagata_1 :::"Basis_sigma_locally_finite"::: ) ))) "holds" (Bool (Set (Var "T")) "is" ($#v10_pre_topc :::"normal"::: ) )) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "F", "G" be ($#m1_subset_1 :::"RealMap":::) "of" (Set (Const "T")); :: original: :::"+"::: redefine func "F" :::"+"::: "G" -> ($#m1_subset_1 :::"RealMap":::) "of" "T" means :: NAGATA_1:def 7 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" "T" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" "G" ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" )))); end; :: deftheorem defines :::"+"::: NAGATA_1:def 7 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_nagata_1 :::"+"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" )))) ")" ))); theorem :: NAGATA_1:21 (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_subset_1 :::"RealMap":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_pscomp_1 :::"continuous"::: ) )) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v1_pscomp_1 :::"continuous"::: ) )))) ; theorem :: NAGATA_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")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_pscomp_1 :::"continuous"::: ) ) & (Bool (Set (Var "G")) "is" ($#v1_pscomp_1 :::"continuous"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k3_nagata_1 :::"+"::: ) (Set (Var "G"))) "is" ($#v1_pscomp_1 :::"continuous"::: ) ))) ; theorem :: NAGATA_1:23 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "ADD")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "ADD")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k3_nagata_1 :::"+"::: ) (Set (Var "f2")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "ADD")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "ADD")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "ADD")) "is" ($#v2_binop_1 :::"associative"::: ) ) ")" ))) ; theorem :: NAGATA_1:24 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "ADD")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "ADD")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k3_nagata_1 :::"+"::: ) (Set (Var "f2")))) ")" )) "holds" (Bool "for" (Set (Var "map9")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool (Bool (Set (Var "map9")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "ADD")))) "holds" (Bool (Set (Var "map9")) "is" ($#v1_pscomp_1 :::"continuous"::: ) )))) ; definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Const "A")) "," (Set (Const "B")) ")" ")" ); func "F" :::"Toler"::: -> ($#m1_subset_1 :::"Function":::) "of" "A" "," "B" means :: NAGATA_1:def 8 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))))); end; :: deftheorem defines :::"Toler"::: NAGATA_1:def 8 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k4_nagata_1 :::"Toler"::: ) )) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))))) ")" )))); theorem :: NAGATA_1:25 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "ADD")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "ADD")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k3_nagata_1 :::"+"::: ) (Set (Var "f2")))) ")" )) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#v1_pscomp_1 :::"continuous"::: ) ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T"))) ")" )) "holds" (Bool (Set (Set (Var "ADD")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F"))) "is" ($#v1_pscomp_1 :::"continuous"::: ) ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T")))))) ; theorem :: NAGATA_1:26 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) ")" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T1"))) ")" )) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "q")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p")))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "F")) ($#k4_nagata_1 :::"Toler"::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#m1_subset_1 :::"Real":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"min"::: "(" "r" "," "f" ")" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: NAGATA_1:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" "r" "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ))); end; :: deftheorem defines :::"min"::: NAGATA_1:def 9 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_nagata_1 :::"min"::: ) "(" (Set (Var "r")) "," (Set (Var "f")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set (Var "r")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ))) ")" )))); theorem :: NAGATA_1:27 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_pscomp_1 :::"continuous"::: ) )) "holds" (Bool (Set ($#k5_nagata_1 :::"min"::: ) "(" (Set (Var "r")) "," (Set (Var "f")) ")" ) "is" ($#v1_pscomp_1 :::"continuous"::: ) )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); pred "f" :::"is_a_pseudometric_of"::: "X" means :: NAGATA_1:def 10 (Bool "(" (Bool "f" "is" ($#v2_metric_1 :::"Reflexive"::: ) ) & (Bool "f" "is" ($#v4_metric_1 :::"symmetric"::: ) ) & (Bool "f" "is" ($#v5_metric_1 :::"triangle"::: ) ) ")" ); end; :: deftheorem defines :::"is_a_pseudometric_of"::: NAGATA_1:def 10 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_metric_1 :::"Reflexive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v4_metric_1 :::"symmetric"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_metric_1 :::"triangle"::: ) ) ")" ) ")" ))); theorem :: NAGATA_1:28 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set (Var "X"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 "c")) "," (Set (Var "b")) ")" ")" ))) ")" )) ")" ))) ; theorem :: NAGATA_1:29 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: NAGATA_1:30 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))))) "holds" (Bool (Set ($#k5_nagata_1 :::"min"::: ) "(" (Set (Var "r")) "," (Set (Var "m")) ")" ) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))))))) ; theorem :: NAGATA_1:31 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))))) "holds" (Bool (Set ($#k5_nagata_1 :::"min"::: ) "(" (Set (Var "r")) "," (Set (Var "m")) ")" ) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))))))) ;