:: NORMSP_2 semantic presentation begin theorem :: NORMSP_2:1 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v4_tbsp_1 :::"complete"::: ) ) & (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "Y")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "X")))) ")" )) "holds" (Bool "ex" (Set (Var "n0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::)(Bool "ex" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x0")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Y")) ($#k8_nat_1 :::"."::: ) (Set (Var "n0")))) ")" )))))) ; begin definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); func :::"distance_by_norm_of"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: NORMSP_2:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "holds" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))); end; :: deftheorem defines :::"distance_by_norm_of"::: NORMSP_2:def 1 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_2 :::"distance_by_norm_of"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b2")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))) ")" ))); definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); func :::"MetricSpaceNorm"::: "X" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) equals :: NORMSP_2:def 2 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "(" ($#k1_normsp_2 :::"distance_by_norm_of"::: ) "X" ")" ) "#)" ); end; :: deftheorem defines :::"MetricSpaceNorm"::: NORMSP_2:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set ($#k2_normsp_2 :::"MetricSpaceNorm"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "(" ($#k1_normsp_2 :::"distance_by_norm_of"::: ) (Set (Var "X")) ")" ) "#)" ))); theorem :: NORMSP_2:2 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_normsp_2 :::"MetricSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "z")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" ) ")" ))))) ; theorem :: NORMSP_2:3 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_normsp_2 :::"MetricSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set ($#k10_metric_1 :::"cl_Ball"::: ) "(" (Set (Var "z")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) "}" ) ")" ))))) ; theorem :: NORMSP_2:4 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k2_normsp_2 :::"MetricSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "xt")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k2_normsp_2 :::"MetricSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "St"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "xt")))) "holds" (Bool "(" (Bool (Set (Var "St")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "xt"))) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "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 ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" )))))) ; theorem :: NORMSP_2:5 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k2_normsp_2 :::"MetricSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "St")))) "holds" (Bool "(" (Bool (Set (Var "St")) "is" ($#v2_tbsp_1 :::"convergent"::: ) ) "iff" (Bool (Set (Var "S")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) ")" )))) ; theorem :: NORMSP_2:6 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k2_normsp_2 :::"MetricSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "St"))) & (Bool (Set (Var "St")) "is" ($#v2_tbsp_1 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_tbsp_1 :::"lim"::: ) (Set (Var "St"))) ($#r1_hidden :::"="::: ) (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "S"))))))) ; begin definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); func :::"TopSpaceNorm"::: "X" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) equals :: NORMSP_2:def 3 (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k2_normsp_2 :::"MetricSpaceNorm"::: ) "X" ")" )); end; :: deftheorem defines :::"TopSpaceNorm"::: NORMSP_2:def 3 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k2_normsp_2 :::"MetricSpaceNorm"::: ) (Set (Var "X")) ")" )))); theorem :: NORMSP_2:7 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" ))) ")" ))) ; theorem :: NORMSP_2:8 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ))))) ; theorem :: NORMSP_2:9 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) "}" "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ))))) ; theorem :: NORMSP_2:10 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"Hausdorff"::: ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v6_waybel_3 :::"locally-compact"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v2_yellow_8 :::"Baire"::: ) )) ; theorem :: NORMSP_2:11 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X"))) "is" ($#v4_frechet :::"sequential"::: ) )) ; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k3_normsp_2 :::"TopSpaceNorm"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_frechet :::"sequential"::: ) ; end; theorem :: NORMSP_2:12 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "xt")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "St"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "xt")))) "holds" (Bool "(" (Bool (Set (Var "St")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "xt"))) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "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 ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" )))))) ; theorem :: NORMSP_2:13 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "St")))) "holds" (Bool "(" (Bool (Set (Var "St")) "is" ($#v2_frechet :::"convergent"::: ) ) "iff" (Bool (Set (Var "S")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) ")" )))) ; theorem :: NORMSP_2:14 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "St"))) & (Bool (Set (Var "St")) "is" ($#v2_frechet :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "St"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k6_normsp_1 :::"lim"::: ) (Set (Var "S")) ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set ($#k2_frechet2 :::"lim"::: ) (Set (Var "St"))) ($#r1_hidden :::"="::: ) (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "S")))) ")" )))) ; theorem :: NORMSP_2:15 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Vt")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "Vt")))) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v2_nfcont_1 :::"closed"::: ) ) "iff" (Bool (Set (Var "Vt")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )))) ; theorem :: NORMSP_2:16 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Vt")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "Vt")))) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v3_nfcont_1 :::"open"::: ) ) "iff" (Bool (Set (Var "Vt")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )))) ; theorem :: NORMSP_2:17 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Ut")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "xt")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "U")) ($#r1_hidden :::"="::: ) (Set (Var "Ut"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "xt")))) "holds" (Bool "(" (Bool (Set (Var "U")) "is" ($#m1_nfcont_1 :::"Neighbourhood"::: ) "of" (Set (Var "x"))) "iff" (Bool (Set (Var "Ut")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "xt"))) ")" )))))) ; theorem :: NORMSP_2:18 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "ft")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "xt")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "ft"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "xt")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_nfcont_1 :::"is_continuous_in"::: ) (Set (Var "x"))) "iff" (Bool (Set (Var "ft")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "xt"))) ")" )))))) ; theorem :: NORMSP_2:19 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "ft")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "Y")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "ft")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_nfcont_1 :::"is_continuous_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) "iff" (Bool (Set (Var "ft")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )))) ; begin definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); func :::"LinearTopSpaceNorm"::: "X" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_rltopsp1 :::"strict"::: ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) means :: NORMSP_2:def 4 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X")) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "X")) & (Bool (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" "X")) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) "X" ")" ))) ")" ); end; :: deftheorem defines :::"LinearTopSpaceNorm"::: NORMSP_2:def 4 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_rltopsp1 :::"strict"::: ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b2"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "X")))) & (Bool (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "b2"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "X")))) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ))) ")" ) ")" ))); registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v5_rltopsp1 :::"strict"::: ) ($#v6_rltopsp1 :::"add-continuous"::: ) ($#v7_rltopsp1 :::"Mult-continuous"::: ) ; end; theorem :: NORMSP_2:20 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "Vt")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "Vt")))) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set (Var "Vt")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )))) ; theorem :: NORMSP_2:21 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "Vt")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "Vt")))) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool (Set (Var "Vt")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )))) ; theorem :: NORMSP_2:22 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" ))) ")" ))) ; theorem :: NORMSP_2:23 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" )) "holds" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ))))) ; theorem :: NORMSP_2:24 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) "}" )) "holds" (Bool (Set (Var "V")) "is" ($#v4_pre_topc :::"closed"::: ) ))))) ; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"T_2"::: ) ($#v5_rltopsp1 :::"strict"::: ) ; cluster (Set ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_8 :::"sober"::: ) ($#v5_rltopsp1 :::"strict"::: ) ; end; theorem :: NORMSP_2:25 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "xt")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "St"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "xt")))) "holds" (Bool "(" (Bool (Set (Var "St")) "is" ($#m1_subset_1 :::"Basis":::) "of" ) "iff" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Basis":::) "of" ) ")" )))))) ; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_frechet :::"first-countable"::: ) ($#v5_rltopsp1 :::"strict"::: ) ; cluster (Set ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_frechet :::"Frechet"::: ) ($#v5_rltopsp1 :::"strict"::: ) ; cluster (Set ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_frechet :::"sequential"::: ) ($#v5_rltopsp1 :::"strict"::: ) ; end; theorem :: NORMSP_2:26 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "xt")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "St"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "xt")))) "holds" (Bool "(" (Bool (Set (Var "St")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "xt"))) "iff" (Bool (Set (Var "S")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x"))) ")" )))))) ; theorem :: NORMSP_2:27 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "St")))) "holds" (Bool "(" (Bool (Set (Var "St")) "is" ($#v2_frechet :::"convergent"::: ) ) "iff" (Bool (Set (Var "S")) "is" ($#v2_frechet :::"convergent"::: ) ) ")" )))) ; theorem :: NORMSP_2:28 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "St"))) & (Bool (Set (Var "St")) "is" ($#v2_frechet :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "St")))) & (Bool (Set ($#k2_frechet2 :::"lim"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k2_frechet2 :::"lim"::: ) (Set (Var "St")))) ")" )))) ; theorem :: NORMSP_2:29 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "xt")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "St"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "xt")))) "holds" (Bool "(" (Bool (Set (Var "St")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "xt"))) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "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 ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" )))))) ; theorem :: NORMSP_2:30 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "St")))) "holds" (Bool "(" (Bool (Set (Var "St")) "is" ($#v2_frechet :::"convergent"::: ) ) "iff" (Bool (Set (Var "S")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) ")" )))) ; theorem :: NORMSP_2:31 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "St"))) & (Bool (Set (Var "St")) "is" ($#v2_frechet :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "St"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k6_normsp_1 :::"lim"::: ) (Set (Var "S")) ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set ($#k2_frechet2 :::"lim"::: ) (Set (Var "St"))) ($#r1_hidden :::"="::: ) (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "S")))) ")" )))) ; theorem :: NORMSP_2:32 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Vt")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "Vt")))) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v2_nfcont_1 :::"closed"::: ) ) "iff" (Bool (Set (Var "Vt")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )))) ; theorem :: NORMSP_2:33 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Vt")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "Vt")))) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v3_nfcont_1 :::"open"::: ) ) "iff" (Bool (Set (Var "Vt")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )))) ; theorem :: NORMSP_2:34 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "Ut")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "xt")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "U")) ($#r1_hidden :::"="::: ) (Set (Var "Ut"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "xt")))) "holds" (Bool "(" (Bool (Set (Var "U")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) "iff" (Bool (Set (Var "Ut")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "xt"))) ")" )))))) ; theorem :: NORMSP_2:35 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "ft")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "xt")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "ft"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "xt")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))) "iff" (Bool (Set (Var "ft")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "xt"))) ")" )))))) ; theorem :: NORMSP_2:36 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "ft")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "Y")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "ft")))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool (Set (Var "ft")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )))) ;