Volume 11, 1999

University of Bialystok

Copyright (c) 1999 Association of Mizar Users

### The abstract of the Mizar article:

### The Sequential Closure Operator in Sequential and Frechet Spaces

**by****Bartlomiej Skorulski**- Received February 13, 1999
- MML identifier: FRECHET2

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_1, FUNCT_1, PRE_TOPC, URYSOHN1, NORMSP_1, FUNCOP_1, FRECHET, BOOLE, COMPTS_1, ORDINAL2, SEQM_3, SEQ_1, ARYTM_1, SQUARE_1, CANTOR_1, CARD_4, SETFAM_1, ORDINAL1, FINSET_1, SEQ_2, METRIC_1, PCOMPS_1, METRIC_6, WAYBEL_7, TARSKI, FUNCT_2, FRECHET2, RLVECT_3, SGRAPH1, ARYTM; notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, ORDINAL1, ORDINAL2, SETFAM_1, FINSET_1, CARD_4, CQC_SIM1, TOPS_2, RELAT_1, FUNCT_1, FUNCT_2, NORMSP_1, COMPTS_1, URYSOHN1, REAL_1, NAT_1, PRE_CIRC, LIMFUNC1, CANTOR_1, SEQ_1, SEQM_3, METRIC_1, PCOMPS_1, TBSP_1, STRUCT_0, PRE_TOPC, FINSOP_1, METRIC_6, YELLOW_8, FRECHET; constructors CARD_4, URYSOHN1, WAYBEL_3, COMPTS_1, TOPS_2, CANTOR_1, SEQ_1, NAT_1, FINSOP_1, PRE_CIRC, CQC_SIM1, INT_1, LIMFUNC1, TBSP_1, METRIC_6, YELLOW_8, FRECHET; clusters XREAL_0, STRUCT_0, PRE_TOPC, NORMSP_1, INT_1, FUNCT_1, METRIC_1, PCOMPS_1, GROUP_2, WAYBEL12, FRECHET, RELSET_1, SEQM_3, FUNCT_2, MEMBERED, NAT_1, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin definition let T be non empty 1-sorted,f be Function of NAT,NAT, S be sequence of T; redefine func S*f -> sequence of T; end; theorem :: FRECHET2:1 for T being non empty 1-sorted, S being sequence of T, NS being increasing Seq_of_Nat holds S*NS is sequence of T; theorem :: FRECHET2:2 for RS being Real_Sequence st RS=id NAT holds RS is increasing Seq_of_Nat; definition let T be non empty 1-sorted, S be sequence of T; mode subsequence of S -> sequence of T means :: FRECHET2:def 1 ex NS being increasing Seq_of_Nat st it = S * NS; end; theorem :: FRECHET2:3 for T being non empty 1-sorted, S being sequence of T holds S is subsequence of S; theorem :: FRECHET2:4 for T being non empty 1-sorted, S being sequence of T, S1 being subsequence of S holds rng S1 c= rng S; definition let T be non empty 1-sorted, NS be increasing Seq_of_Nat, S be sequence of T; redefine func S*NS -> subsequence of S; end; theorem :: FRECHET2:5 for T being non empty 1-sorted, S1 being sequence of T, S2 being subsequence of S1, S3 being subsequence of S2 holds S3 is subsequence of S1; scheme SubSeqChoice {T()->non empty 1-sorted,S()->sequence of T(),P[set]} : ex S1 being subsequence of S() st for n being Nat holds P[S1.n] provided for n being Nat ex m being Nat,x being Point of T() st n <= m & x = S().m & P[x]; scheme SubSeqChoice1 {T()->non empty TopStruct,S()->sequence of T(),P[set]} : ex S1 being subsequence of S() st for n being Nat holds P[S1.n] provided for n being Nat ex m being Nat,x being Point of T() st n <= m & x = S().m & P[x]; theorem :: FRECHET2:6 for T being non empty 1-sorted, S being sequence of T, A being Subset of T holds (for S1 being subsequence of S holds not rng S1 c= A) implies (ex n being Nat st for m being Nat st n <= m holds not S.m in A); theorem :: FRECHET2:7 for T being non empty 1-sorted,S being sequence of T, A,B being Subset of T st rng S c= A \/ B holds ex S1 being subsequence of S st rng S1 c= A or rng S1 c= B; theorem :: FRECHET2:8 for T being non empty TopSpace holds (for S being sequence of T holds for x1,x2 being Point of T holds (x1 in Lim S & x2 in Lim S implies x1=x2)) implies T is_T1; theorem :: FRECHET2:9 for T being non empty TopSpace st T is_T2 holds for S being sequence of T, x1,x2 being Point of T holds (x1 in Lim S & x2 in Lim S implies x1=x2); theorem :: FRECHET2:10 for T being non empty TopSpace st T is first-countable holds T is_T2 iff (for S being sequence of T holds for x1,x2 being Point of T holds (x1 in Lim S & x2 in Lim S implies x1=x2)); theorem :: FRECHET2:11 for T being non empty TopStruct, S being sequence of T st S is not convergent holds Lim S = {}; theorem :: FRECHET2:12 for T being non empty TopSpace,A being Subset of T holds A is closed implies (for S being sequence of T st rng S c= A holds Lim S c= A); theorem :: FRECHET2:13 for T being non empty TopStruct,S being sequence of T, x being Point of T st not S is_convergent_to x holds ex S1 being subsequence of S st for S2 being subsequence of S1 holds not S2 is_convergent_to x; begin ::The Continuous Maps theorem :: FRECHET2:14 for T1,T2 being non empty TopSpace, f being map of T1,T2 holds f is continuous implies for S1 being sequence of T1, S2 being sequence of T2 st S2=f*S1 holds f.:(Lim S1) c= Lim S2; theorem :: FRECHET2:15 for T1,T2 being non empty TopSpace, f being map of T1,T2 st T1 is sequential holds f is continuous iff for S1 being sequence of T1, S2 being sequence of T2 st S2=f*S1 holds f.:(Lim S1) c= Lim S2; begin ::The Sequential Closure Operator definition let T be non empty TopStruct, A be Subset of T; func Cl_Seq A -> Subset of T means :: FRECHET2:def 2 for x being Point of T holds x in it iff ex S being sequence of T st rng S c= A & x in Lim S; end; theorem :: FRECHET2:16 for T being non empty TopStruct, A being Subset of T, S being sequence of T, x being Point of T st rng S c= A & x in Lim S holds x in Cl(A); theorem :: FRECHET2:17 for T being non empty TopStruct, A being Subset of T holds Cl_Seq(A) c= Cl(A); theorem :: FRECHET2:18 for T being non empty TopStruct, S being sequence of T, S1 being subsequence of S, x being Point of T holds S is_convergent_to x implies S1 is_convergent_to x; theorem :: FRECHET2:19 for T being non empty TopStruct, S being sequence of T, S1 being subsequence of S holds Lim S c= Lim S1; theorem :: FRECHET2:20 for T being non empty TopStruct holds Cl_Seq({}T) = {}; theorem :: FRECHET2:21 for T being non empty TopStruct, A being Subset of T holds A c= Cl_Seq(A); theorem :: FRECHET2:22 for T being non empty TopStruct, A,B being Subset of T holds Cl_Seq(A) \/ Cl_Seq(B) = Cl_Seq(A \/ B); theorem :: FRECHET2:23 for T being non empty TopStruct holds T is Frechet iff for A being Subset of T holds Cl(A)=Cl_Seq(A); theorem :: FRECHET2:24 for T being non empty TopSpace st T is Frechet holds for A,B being Subset of T holds Cl_Seq({}T) = {} & A c= Cl_Seq(A) & Cl_Seq(A \/ B) = Cl_Seq(A) \/ Cl_Seq(B) & Cl_Seq(Cl_Seq(A)) = Cl_Seq(A); theorem :: FRECHET2:25 for T being non empty TopSpace st T is sequential holds (for A being Subset of T holds Cl_Seq(Cl_Seq(A)) = Cl_Seq(A)) implies T is Frechet; theorem :: FRECHET2:26 for T being non empty TopSpace st T is sequential holds T is Frechet iff for A,B being Subset of T holds Cl_Seq({}T) = {} & A c= Cl_Seq(A) & Cl_Seq(A \/ B) = Cl_Seq(A) \/ Cl_Seq(B) & Cl_Seq(Cl_Seq(A)) = Cl_Seq(A); begin ::The Limit definition let T be non empty TopSpace, S be sequence of T; assume that ex x being Point of T st Lim S = {x}; func lim S -> Point of T means :: FRECHET2:def 3 S is_convergent_to it; end; theorem :: FRECHET2:27 for T being non empty TopSpace st T is_T2 for S being sequence of T st S is convergent holds ex x being Point of T st Lim S = {x}; theorem :: FRECHET2:28 for T being non empty TopSpace st T is_T2 for S being sequence of T,x being Point of T holds S is_convergent_to x iff S is convergent & x = lim S; theorem :: FRECHET2:29 for M being MetrStruct,S being sequence of M holds S is sequence of TopSpaceMetr(M); theorem :: FRECHET2:30 for M being non empty MetrStruct,S being sequence of TopSpaceMetr(M) holds S is sequence of M; theorem :: FRECHET2:31 for M being non empty MetrSpace,S being sequence of M, x being Point of M, S' being sequence of TopSpaceMetr(M), x' being Point of TopSpaceMetr(M) st S = S' & x = x' holds S is_convergent_in_metrspace_to x iff S' is_convergent_to x'; theorem :: FRECHET2:32 for M being non empty MetrSpace,Sm being sequence of M, St being sequence of TopSpaceMetr(M) st Sm=St holds Sm is convergent iff St is convergent; theorem :: FRECHET2:33 for M being non empty MetrSpace,Sm being sequence of M, St being sequence of TopSpaceMetr(M) st Sm=St & Sm is convergent holds lim Sm = lim St; begin ::The Cluster Points definition let T be TopStruct, S be sequence of T, x be Point of T; pred x is_a_cluster_point_of S means :: FRECHET2:def 4 for O being Subset of T, n being Nat st O is open & x in O ex m being Nat st n <= m & S.m in O; end; theorem :: FRECHET2:34 for T being non empty TopStruct, S being sequence of T, x being Point of T st ex S1 being subsequence of S st S1 is_convergent_to x holds x is_a_cluster_point_of S; theorem :: FRECHET2:35 for T being non empty TopStruct, S being sequence of T, x being Point of T st S is_convergent_to x holds x is_a_cluster_point_of S; theorem :: FRECHET2:36 for T being non empty TopStruct, S being sequence of T, x being Point of T, Y being Subset of T st Y = {y where y is Point of T : x in Cl({y}) } & rng S c= Y holds S is_convergent_to x; theorem :: FRECHET2:37 for T being non empty TopStruct, S being sequence of T, x,y being Point of T st for n being Nat holds S.n = y & S is_convergent_to x holds x in Cl({y}); theorem :: FRECHET2:38 for T being non empty TopStruct, x being Point of T, Y being Subset of T, S being sequence of T st Y = { y where y is Point of T : x in Cl({y}) } & rng S misses Y & S is_convergent_to x ex S1 being subsequence of S st S1 is one-to-one; theorem :: FRECHET2:39 for T being non empty TopStruct, S1,S2 being sequence of T st rng S2 c= rng S1 & S2 is one-to-one ex P being Permutation of NAT st S2*P is subsequence of S1; scheme PermSeq {T()->non empty 1-sorted,S()->sequence of T(),p()->Permutation of NAT, P[set]} : ex n being Nat st for m being Nat st n<=m holds P[(S()*p()).m] provided ex n being Nat st for m being Nat, x being Point of T() st n<=m & x=S().m holds P[x]; scheme PermSeq2 {T()->non empty TopStruct,S()->sequence of T(),p()->Permutation of NAT, P[set]} : ex n being Nat st for m being Nat st n<=m holds P[(S()*p()).m] provided ex n being Nat st for m being Nat, x being Point of T() st n<=m & x=S().m holds P[x]; theorem :: FRECHET2:40 for T being non empty TopStruct, S being sequence of T, P being Permutation of NAT, x being Point of T st S is_convergent_to x holds S*P is_convergent_to x; theorem :: FRECHET2:41 for n0 being Nat ex NS being increasing Seq_of_Nat st for n being Nat holds NS.n=n+n0; theorem :: FRECHET2:42 for T being non empty 1-sorted, S being sequence of T, n0 being Nat ex S1 being subsequence of S st for n being Nat holds S1.n=S.(n+n0); theorem :: FRECHET2:43 for T being non empty TopStruct, S being sequence of T, x being Point of T, S1 being subsequence of S st x is_a_cluster_point_of S & ex n0 being Nat st for n being Nat holds S1.n=S.(n+n0) holds x is_a_cluster_point_of S1; theorem :: FRECHET2:44 for T being non empty TopStruct, S being sequence of T, x being Point of T st x is_a_cluster_point_of S holds x in Cl(rng S); theorem :: FRECHET2:45 for T being non empty TopStruct st T is Frechet for S being sequence of T, x being Point of T st x is_a_cluster_point_of S holds ex S1 being subsequence of S st S1 is_convergent_to x; begin :: Auxiliary theorems theorem :: FRECHET2:46 for T being non empty TopSpace st T is first-countable holds for x being Point of T holds ex B being Basis of x st ex S being Function st dom S = NAT & rng S = B & for n,m being Nat st m >= n holds S.m c= S.n; theorem :: FRECHET2:47 for T being non empty TopSpace holds T is_T1 iff for p being Point of T holds Cl({p}) = {p}; theorem :: FRECHET2:48 for T being non empty TopSpace holds T is_T2 implies T is_T1; theorem :: FRECHET2:49 for T being non empty TopSpace st not T is_T1 holds ex x1,x2 being Point of T, S being sequence of T st S = (NAT --> x1) & x1 <> x2 & S is_convergent_to x2; theorem :: FRECHET2:50 for f being Function st dom f is infinite & f is one-to-one holds rng f is infinite; theorem :: FRECHET2:51 for X being non empty finite Subset of NAT, x being Nat holds x in X implies x <= max X;

Back to top