:: FRECHET2 semantic presentation begin theorem :: FRECHET2:1 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "NS")) "being" ($#v5_valued_0 :::"increasing"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "S")) ($#k2_valued_0 :::"*"::: ) (Set (Var "NS"))) "is" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")))))) ; theorem :: FRECHET2:2 (Bool "for" (Set (Var "RS")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "RS")) ($#r1_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))) "holds" (Bool (Set (Var "RS")) "is" ($#v5_valued_0 :::"increasing"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: FRECHET2:3 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "S1")) "being" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "S")) "holds" (Bool (Bool "not" (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S1"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) ")" )) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "not" (Bool (Set (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))))))) ; theorem :: FRECHET2:4 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "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 ($#k2_relset_1 :::"rng"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))))) "holds" (Bool "ex" (Set (Var "S1")) "being" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S1"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "or" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S1"))) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) ")" ))))) ; theorem :: FRECHET2:5 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S")))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))) ")" )) "holds" (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) )) ; theorem :: FRECHET2:6 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_pre_topc :::"T_2"::: ) )) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S")))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))))) ; theorem :: FRECHET2:7 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v1_frechet :::"first-countable"::: ) )) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v8_pre_topc :::"T_2"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S")))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))))) ")" )) ; theorem :: FRECHET2:8 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Bool "not" (Set (Var "S")) "is" ($#v2_frechet :::"convergent"::: ) ))) "holds" (Bool (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: FRECHET2:9 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))))) ; theorem :: FRECHET2:10 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Bool "not" (Set (Var "S")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x"))))) "holds" (Bool "ex" (Set (Var "S1")) "being" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "S")) "st" (Bool "for" (Set (Var "S2")) "being" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "S1")) "holds" (Bool (Bool "not" (Set (Var "S2")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x"))))))))) ; begin theorem :: FRECHET2:11 (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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "for" (Set (Var "S1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "S2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T2")) "st" (Bool (Bool (Set (Var "S2")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "S1"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_frechet :::"Lim"::: ) (Set (Var "S1")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S2")))))))) ; theorem :: FRECHET2:12 (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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) "st" (Bool (Bool (Set (Var "T1")) "is" ($#v4_frechet :::"sequential"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "S1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "S2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T2")) "st" (Bool (Bool (Set (Var "S2")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "S1"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_frechet :::"Lim"::: ) (Set (Var "S1")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S2")))))) ")" ))) ; begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func :::"Cl_Seq"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "T" means :: FRECHET2:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" "T" "st" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) "A") & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S")))) ")" )) ")" )); end; :: deftheorem defines :::"Cl_Seq"::: FRECHET2:def 1 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S")))) ")" )) ")" )) ")" ))); theorem :: FRECHET2:13 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))))))) ; theorem :: FRECHET2:14 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))))) ; theorem :: FRECHET2:15 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "S1")) "being" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "S1")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x"))))))) ; theorem :: FRECHET2:16 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "S1")) "being" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S1"))))))) ; theorem :: FRECHET2:17 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: FRECHET2:18 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A")))))) ; theorem :: FRECHET2:19 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ))))) ; theorem :: FRECHET2:20 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v3_frechet :::"Frechet"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A"))))) ")" )) ; theorem :: FRECHET2: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_frechet :::"Frechet"::: ) )) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A")))) & (Bool (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "B")) ")" ))) & (Bool (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set "(" ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A")))) ")" ))) ; theorem :: FRECHET2:22 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v4_frechet :::"sequential"::: ) ) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set "(" ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A")))) ")" )) "holds" (Bool (Set (Var "T")) "is" ($#v3_frechet :::"Frechet"::: ) )) ; theorem :: FRECHET2:23 (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" ($#v4_frechet :::"sequential"::: ) )) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v3_frechet :::"Frechet"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A")))) & (Bool (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "B")) ")" ))) & (Bool (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set "(" ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_frechet2 :::"Cl_Seq"::: ) (Set (Var "A")))) ")" )) ")" )) ; begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "S" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "T")); assume (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")) "st" (Bool (Set ($#k2_frechet :::"Lim"::: ) (Set (Const "S"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))) ; func :::"lim"::: "S" -> ($#m1_subset_1 :::"Point":::) "of" "T" means :: FRECHET2:def 2 (Bool "S" ($#r1_frechet :::"is_convergent_to"::: ) it); end; :: deftheorem defines :::"lim"::: FRECHET2:def 2 : (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 :::"sequence":::) "of" (Set (Var "T")) "st" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_frechet2 :::"lim"::: ) (Set (Var "S")))) "iff" (Bool (Set (Var "S")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "b3"))) ")" )))); theorem :: FRECHET2:24 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_pre_topc :::"T_2"::: ) )) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v2_frechet :::"convergent"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Set ($#k2_frechet :::"Lim"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: FRECHET2:25 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_pre_topc :::"T_2"::: ) )) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x"))) "iff" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_frechet :::"convergent"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_frechet2 :::"lim"::: ) (Set (Var "S")))) ")" ) ")" )))) ; theorem :: FRECHET2:26 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "M")) "holds" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" )))) ; theorem :: FRECHET2:27 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "holds" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "M"))))) ; theorem :: FRECHET2:28 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "S9")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "x9")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "S9"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9")))) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x"))) "iff" (Bool (Set (Var "S9")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x9"))) ")" )))))) ; theorem :: FRECHET2:29 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "Sm")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "Sm")) ($#r1_funct_2 :::"="::: ) (Set (Var "St")))) "holds" (Bool "(" (Bool (Set (Var "Sm")) "is" ($#v2_tbsp_1 :::"convergent"::: ) ) "iff" (Bool (Set (Var "St")) "is" ($#v2_frechet :::"convergent"::: ) ) ")" )))) ; theorem :: FRECHET2:30 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "Sm")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "St")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "Sm")) ($#r1_funct_2 :::"="::: ) (Set (Var "St"))) & (Bool (Set (Var "Sm")) "is" ($#v2_tbsp_1 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_tbsp_1 :::"lim"::: ) (Set (Var "Sm"))) ($#r1_hidden :::"="::: ) (Set ($#k2_frechet2 :::"lim"::: ) (Set (Var "St"))))))) ; begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "S" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "T")); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); pred "x" :::"is_a_cluster_point_of"::: "S" means :: FRECHET2:def 3 (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "O")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool "x" ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set "S" ($#k8_nat_1 :::"."::: ) (Set (Var "m"))) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) ")" )))); end; :: deftheorem defines :::"is_a_cluster_point_of"::: FRECHET2:def 3 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_frechet2 :::"is_a_cluster_point_of"::: ) (Set (Var "S"))) "iff" (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "O")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) ")" )))) ")" )))); theorem :: FRECHET2:31 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool "ex" (Set (Var "S1")) "being" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "S")) "st" (Bool (Set (Var "S1")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "x")) ($#r1_frechet2 :::"is_a_cluster_point_of"::: ) (Set (Var "S")))))) ; theorem :: FRECHET2:32 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "x")) ($#r1_frechet2 :::"is_a_cluster_point_of"::: ) (Set (Var "S")))))) ; theorem :: FRECHET2:33 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ))) "}" ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "S")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x"))))))) ; theorem :: FRECHET2:34 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "S")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x"))) ")" ) ")" )) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: FRECHET2:35 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ))) "}" ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y"))) & (Bool (Set (Var "S")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x")))) "holds" (Bool "ex" (Set (Var "S1")) "being" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "S")) "st" (Bool (Set (Var "S1")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )))))) ; theorem :: FRECHET2:36 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S2"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S1")))) & (Bool (Set (Var "S2")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "S2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "P"))) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "S1")))))) ; scheme :: FRECHET2:sch 1 PermSeq{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) , F2() -> ($#m1_subset_1 :::"sequence":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Permutation":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool P1[(Set (Set "(" (Set F2 "(" ")" ) ($#k1_partfun1 :::"*"::: ) (Set F3 "(" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))]))) provided (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))))) "holds" (Bool P1[(Set (Var "x"))])))) proof end; scheme :: FRECHET2:sch 2 PermSeq2{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) , F2() -> ($#m1_subset_1 :::"sequence":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Permutation":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool P1[(Set (Set "(" (Set F2 "(" ")" ) ($#k1_partfun1 :::"*"::: ) (Set F3 "(" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))]))) provided (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))))) "holds" (Bool P1[(Set (Var "x"))])))) proof end; theorem :: FRECHET2:37 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x")))) "holds" (Bool (Set (Set (Var "S")) ($#k1_partfun1 :::"*"::: ) (Set (Var "P"))) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x"))))))) ; theorem :: FRECHET2:38 (Bool "for" (Set (Var "n0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "NS")) "being" ($#v5_valued_0 :::"increasing"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "NS")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n0"))))))) ; theorem :: FRECHET2:39 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "n0")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_frechet2 :::"is_a_cluster_point_of"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "x")) ($#r1_frechet2 :::"is_a_cluster_point_of"::: ) (Set (Set (Var "S")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n0")))))))) ; theorem :: FRECHET2:40 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r1_frechet2 :::"is_a_cluster_point_of"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "S")) ")" )))))) ; theorem :: FRECHET2:41 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_frechet :::"Frechet"::: ) )) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r1_frechet2 :::"is_a_cluster_point_of"::: ) (Set (Var "S")))) "holds" (Bool "ex" (Set (Var "S1")) "being" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "S")) "st" (Bool (Set (Var "S1")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x"))))))) ; begin theorem :: FRECHET2:42 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v1_frechet :::"first-countable"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x"))(Bool "ex" (Set (Var "S")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool "(" "for" (Set (Var "n")) "," (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 "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" ))))) ; theorem :: FRECHET2:43 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ")" )) "holds" (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) )) ; theorem :: FRECHET2:44 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_pre_topc :::"T_2"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) )) ; theorem :: FRECHET2:45 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Bool "not" (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) ))) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))(Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "S")) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "x1")))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "S")) ($#r1_frechet :::"is_convergent_to"::: ) (Set (Var "x2"))) ")" )))) ;