:: NAGATA_2 semantic presentation begin theorem :: NAGATA_2:1 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))) ; definitionfunc :::"PairFunc"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) means :: NAGATA_2:def 1 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "m")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)))); end; :: deftheorem defines :::"PairFunc"::: NAGATA_2:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_nagata_2 :::"PairFunc"::: ) )) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "n")) "," (Set (Var "m")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)))) ")" )); theorem :: NAGATA_2:2 (Bool (Set ($#k1_nagata_2 :::"PairFunc"::: ) ) "is" ($#v3_funct_2 :::"bijective"::: ) ) ; 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"::: ) ); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); func :::"dist"::: "(" "f" "," "x" ")" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: NAGATA_2:def 2 (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_metric_1 :::"."::: ) "(" "x" "," (Set (Var "y")) ")" ))); end; :: deftheorem defines :::"dist"::: NAGATA_2:def 2 : (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"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (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 ($#k2_nagata_2 :::"dist"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))) ")" ))))); theorem :: NAGATA_2:3 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "D")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T2")) (Bool "for" (Set (Var "X1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "X2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "X1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_funct_3 :::"pr1"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "D")) ($#k8_subset_1 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x2")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )))) "implies" (Bool (Set (Var "X1")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" & "(" (Bool (Bool (Set (Var "X2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "D")) ($#k8_subset_1 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x1")) ($#k6_domain_1 :::"}"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )))) "implies" (Bool (Set (Var "X2")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ")" ))))))) ; theorem :: NAGATA_2:4 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "pmet")) "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 "(" "for" (Set (Var "pmet9")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "pmet")) ($#r1_funct_2 :::"="::: ) (Set (Var "pmet9")))) "holds" (Bool (Set (Var "pmet9")) "is" ($#v1_pscomp_1 :::"continuous"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_nagata_2 :::"dist"::: ) "(" (Set (Var "pmet")) "," (Set (Var "x")) ")" ) "is" ($#v1_pscomp_1 :::"continuous"::: ) )))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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"::: ) ); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); func :::"lower_bound"::: "(" "f" "," "A" ")" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: NAGATA_2:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set "(" ($#k2_nagata_2 :::"dist"::: ) "(" "f" "," (Set (Var "x")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) "A" ")" )))); end; :: deftheorem defines :::"lower_bound"::: NAGATA_2:def 3 : (Bool "for" (Set (Var "X")) "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 "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (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 ($#k3_nagata_2 :::"lower_bound"::: ) "(" (Set (Var "f")) "," (Set (Var "A")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set "(" ($#k2_nagata_2 :::"dist"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" )))) ")" ))))); theorem :: NAGATA_2:5 (Bool "for" (Set (Var "X")) "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 "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 "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k3_nagata_2 :::"lower_bound"::: ) "(" (Set (Var "f")) "," (Set (Var "A")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: NAGATA_2:6 (Bool "for" (Set (Var "X")) "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 "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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" ($#k3_nagata_2 :::"lower_bound"::: ) "(" (Set (Var "f")) "," (Set (Var "A")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: NAGATA_2:7 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "pmet")) "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 "pmet")) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" ($#k3_nagata_2 :::"lower_bound"::: ) "(" (Set (Var "pmet")) "," (Set (Var "A")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_nagata_2 :::"lower_bound"::: ) "(" (Set (Var "pmet")) "," (Set (Var "A")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "pmet")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))))) ; theorem :: NAGATA_2:8 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "pmet")) "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 "pmet")) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_nagata_2 :::"dist"::: ) "(" (Set (Var "pmet")) "," (Set (Var "p")) ")" ) "is" ($#v1_pscomp_1 :::"continuous"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k3_nagata_2 :::"lower_bound"::: ) "(" (Set (Var "pmet")) "," (Set (Var "A")) ")" ) "is" ($#v1_pscomp_1 :::"continuous"::: ) )))) ; theorem :: NAGATA_2:9 (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_pcomps_1 :::"is_metric_of"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "f")) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set (Var "X"))))) ; theorem :: NAGATA_2:10 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "pmet")) "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 "pmet")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) & (Bool "(" "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) : (Bool (Set (Set "(" ($#k3_nagata_2 :::"lower_bound"::: ) "(" (Set (Var "pmet")) "," (Set (Var "A")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ) ")" )) "holds" (Bool (Set (Var "T")) "is" ($#v3_pcomps_1 :::"metrizable"::: ) ))) ; theorem :: NAGATA_2:11 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FS2")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "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 "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "pmet")) "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 (Set (Var "FS2")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Var "pmet"))) & (Bool (Set (Var "pmet")) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "pq")) "being" ($#m1_subset_1 :::"Element"::: ) "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 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "FS2")) ($#k10_seqfunc :::"#"::: ) (Set (Var "pq"))) "is" ($#v1_series_1 :::"summable"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "pmet")) "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 "(" "for" (Set (Var "pq")) "being" ($#m1_subset_1 :::"Element"::: ) "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 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "pmet")) ($#k3_funct_2 :::"."::: ) (Set (Var "pq"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "FS2")) ($#k10_seqfunc :::"#"::: ) (Set (Var "pq")) ")" ))) ")" )) "holds" (Bool (Set (Var "pmet")) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))))))) ; theorem :: NAGATA_2:12 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" )) "holds" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))))) ; theorem :: NAGATA_2:13 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))))) ; theorem :: NAGATA_2:14 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "FS1")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (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"::: ) ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Set (Var "FS1")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "f")) "is" ($#v1_pscomp_1 :::"continuous"::: ) ) & (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"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ")" ) & (Bool "ex" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_series_1 :::"summable"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "FS1")) ($#k10_seqfunc :::"#"::: ) (Set (Var "p")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))) ")" ) ")" ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T")) "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"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "FS1")) ($#k10_seqfunc :::"#"::: ) (Set (Var "p")) ")" ))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v1_pscomp_1 :::"continuous"::: ) )))) ; theorem :: NAGATA_2:15 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "FS2")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "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 "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "pmet")) "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 (Set (Var "FS2")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Var "pmet"))) & (Bool (Set (Var "pmet")) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) & (Bool "(" "for" (Set (Var "pq")) "being" ($#m1_subset_1 :::"Element"::: ) "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 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "pmet")) ($#k3_funct_2 :::"."::: ) (Set (Var "pq"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) ")" ) & (Bool "(" "for" (Set (Var "pmet9")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "pmet")) ($#r1_funct_2 :::"="::: ) (Set (Var "pmet9")))) "holds" (Bool (Set (Var "pmet9")) "is" ($#v1_pscomp_1 :::"continuous"::: ) ) ")" ) ")" )) ")" )) "holds" (Bool "for" (Set (Var "pmet")) "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 "(" "for" (Set (Var "pq")) "being" ($#m1_subset_1 :::"Element"::: ) "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 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "pmet")) ($#k3_funct_2 :::"."::: ) (Set (Var "pq"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_prepower :::"GeoSeq"::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "FS2")) ($#k10_seqfunc :::"#"::: ) (Set (Var "pq")) ")" ) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Var "pmet")) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) & (Bool "(" "for" (Set (Var "pmet9")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "pmet")) ($#r1_funct_2 :::"="::: ) (Set (Var "pmet9")))) "holds" (Bool (Set (Var "pmet9")) "is" ($#v1_pscomp_1 :::"continuous"::: ) ) ")" ) ")" ))))) ; theorem :: NAGATA_2:16 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "pmet")) "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 "pmet")) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) & (Bool "(" "for" (Set (Var "pmet9")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "pmet")) ($#r1_funct_2 :::"="::: ) (Set (Var "pmet9")))) "holds" (Bool (Set (Var "pmet9")) "is" ($#v1_pscomp_1 :::"continuous"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" ($#k3_nagata_2 :::"lower_bound"::: ) "(" (Set (Var "pmet")) "," (Set (Var "A")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: NAGATA_2:17 (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" ($#v7_pre_topc :::"T_1"::: ) )) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "FS2")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "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 "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "pmet")) "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 (Set (Var "FS2")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Var "pmet"))) & (Bool (Set (Var "pmet")) ($#r1_nagata_1 :::"is_a_pseudometric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) & (Bool "(" "for" (Set (Var "pq")) "being" ($#m1_subset_1 :::"Element"::: ) "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 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "pmet")) ($#k3_funct_2 :::"."::: ) (Set (Var "pq"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) ")" ) & (Bool "(" "for" (Set (Var "pmet9")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "pmet")) ($#r1_funct_2 :::"="::: ) (Set (Var "pmet9")))) "holds" (Bool (Set (Var "pmet9")) "is" ($#v1_pscomp_1 :::"continuous"::: ) ) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A9")))) & (Bool (Set (Var "A9")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "pmet")) "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 (Set (Var "FS2")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Var "pmet")))) "holds" (Bool (Set (Set "(" ($#k3_nagata_2 :::"lower_bound"::: ) "(" (Set (Var "pmet")) "," (Set (Var "A9")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ")" )) "holds" (Bool "(" (Bool "ex" (Set (Var "pmet")) "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 "pmet")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) & (Bool "(" "for" (Set (Var "pq")) "being" ($#m1_subset_1 :::"Element"::: ) "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 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "pmet")) ($#k3_funct_2 :::"."::: ) (Set (Var "pq"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_prepower :::"GeoSeq"::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "FS2")) ($#k10_seqfunc :::"#"::: ) (Set (Var "pq")) ")" ) ")" ))) ")" ) ")" )) & (Bool (Set (Var "T")) "is" ($#v3_pcomps_1 :::"metrizable"::: ) ) ")" )))) ; theorem :: NAGATA_2:18 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "q")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "q"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) & (Bool (Set (Var "B")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "B")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool "(" (Bool (Set (Var "r")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "q")) ")" ))) & (Bool (Set (Set (Var "B")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "B")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "B")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "r")) ")" ) ")" )) ")" ))))) ; registrationlet "T1", "T2" be ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Const "T1")) "," (Set (Const "T2")) ($#k2_borsuk_1 :::":]"::: ) ); let "t1" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T1")); let "t2" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T2")); cluster (Set "f" ($#k1_binop_1 :::"."::: ) "(" "t1" "," "t2" ")" ) -> ($#v1_xreal_0 :::"real"::: ) ; end; theorem :: NAGATA_2:19 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "T")) "is" ($#v9_pre_topc :::"regular"::: ) ) & (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) ) & (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"::: ) )) ")" ) "iff" (Bool (Set (Var "T")) "is" ($#v3_pcomps_1 :::"metrizable"::: ) ) ")" )) ; theorem :: NAGATA_2: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" ($#v3_pcomps_1 :::"metrizable"::: ) )) "holds" (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"))) & (Bool (Set (Var "FX")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "Un")) "being" ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set ($#k2_nagata_1 :::"Union"::: ) (Set (Var "Un"))) "is" ($#v1_tops_2 :::"open"::: ) ) & (Bool (Set ($#k2_nagata_1 :::"Union"::: ) (Set (Var "Un"))) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) & (Bool (Set ($#k2_nagata_1 :::"Union"::: ) (Set (Var "Un"))) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "FX"))) & (Bool (Set (Var "Un")) "is" ($#v2_nagata_1 :::"sigma_discrete"::: ) ) ")" )))) ; theorem :: NAGATA_2:21 (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" ($#v5_nagata_1 :::"Basis_sigma_discrete"::: ) ))) ; theorem :: NAGATA_2:22 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "T")) "is" ($#v9_pre_topc :::"regular"::: ) ) & (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) ) & (Bool "ex" (Set (Var "Bn")) "being" ($#m1_subset_1 :::"FamilySequence":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "Bn")) "is" ($#v5_nagata_1 :::"Basis_sigma_discrete"::: ) )) ")" ) "iff" (Bool (Set (Var "T")) "is" ($#v3_pcomps_1 :::"metrizable"::: ) ) ")" )) ;