:: The Sequential Closure Operator In Sequential and Frechet Spaces
:: by Bart{\l}omiej Skorulski
::
:: Received February 13, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

Lm1:  for T being non empty TopSpace st ( for p being Point of T holds Cl {p} = {p} ) holds
T is T_1
proofend;

Lm2:  for T being non empty TopSpace st not T is T_1 holds
ex x1, x2 being Point of T st
( x1 <> x2 &amp; x2 in Cl {x1} )
proofend;

Lm3:  for T being non empty TopSpace st not T is T_1 holds
ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 &amp; x1 <> x2 &amp; S is_convergent_to x2 )
proofend;

Lm4:  for T being non empty TopSpace st T is T_2 holds
T is T_1
proofend;

theorem :: FRECHET2:1
for T being non empty 1-sorted
for S being sequence of T
for NS being increasing sequence 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 sequence of NAT ;

theorem Th3: :: FRECHET2:3
for T being non empty 1-sorted
for S being sequence of T
for A being Subset of T st ( for S1 being subsequence of S holds not rng S1 c= A ) holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
not S . m in A
proofend;

theorem Th4: :: FRECHET2:4
for T being non empty 1-sorted
for S being sequence of T
for 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 )
proofend;

Lm5:  for T being non empty TopSpace st T is first-countable holds
for x being Point of T ex B being Basis of x ex S being Function st
( dom S = NAT &amp; rng S = B &amp; ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
proofend;

theorem :: FRECHET2:5
for T being non empty TopSpace st ( for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S &amp; x2 in Lim S holds
x1 = x2 ) holds
T is T_1
proofend;

theorem Th6: :: FRECHET2:6
for T being non empty TopSpace st T is T_2 holds
for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S &amp; x2 in Lim S holds
x1 = x2
proofend;

theorem :: FRECHET2:7
for T being non empty TopSpace st T is first-countable holds
( T is T_2 iff for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S &amp; x2 in Lim S holds
x1 = x2 )
proofend;

theorem :: FRECHET2:8
for T being non empty TopStruct
for S being sequence of T st not S is convergent holds
Lim S = {}
proofend;

theorem Th9: :: FRECHET2:9
for T being non empty TopSpace
for A being Subset of T st A is closed holds
for S being sequence of T st rng S c= A holds
Lim S c= A by FRECHET:24;

theorem :: FRECHET2:10
for T being non empty TopStruct
for S being sequence of T
for 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
proofend;

begin

theorem Th11: :: FRECHET2:11
for T1, T2 being non empty TopSpace
for f being Function of T1,T2 st f is continuous holds
for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2
proofend;

theorem :: FRECHET2:12
for T1, T2 being non empty TopSpace
for f being Function of T1,T2 st T1 is sequential holds
( f is continuous iff for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 )
proofend;

begin

definition
let T be non empty TopStruct ;
let A be Subset of T;
func Cl_Seq A ->  Subset of T means :Def1: :: FRECHET2:def 1
 for x being Point of T holds
( x in it iff ex S being sequence of T st
( rng S c= A &amp; x in Lim S ) );
existence
 ex b1 being Subset of T st
for x being Point of T holds
( x in b1 iff ex S being sequence of T st
( rng S c= A &amp; x in Lim S ) )
proofend;
uniqueness
 for b1, b2 being Subset of T st ( for x being Point of T holds
( x in b1 iff ex S being sequence of T st
( rng S c= A &amp; x in Lim S ) ) ) &amp; ( for x being Point of T holds
( x in b2 iff ex S being sequence of T st
( rng S c= A &amp; x in Lim S ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Cl_Seq FRECHET2:def_1_:_
 for T being non empty TopStruct
for A, b3 being Subset of T holds
( b3 = Cl_Seq A iff for x being Point of T holds
( x in b3 iff ex S being sequence of T st
( rng S c= A &amp; x in Lim S ) ) );

theorem Th13: :: FRECHET2:13
for T being non empty TopStruct
for A being Subset of T
for S being sequence of T
for x being Point of T st rng S c= A &amp; x in Lim S holds
x in Cl A
proofend;

theorem Th14: :: FRECHET2:14
for T being non empty TopStruct
for A being Subset of T holds Cl_Seq A c= Cl A
proofend;

theorem Th15: :: FRECHET2:15
for T being non empty TopStruct
for S being sequence of T
for S1 being subsequence of S
for x being Point of T st S is_convergent_to x holds
S1 is_convergent_to x
proofend;

theorem Th16: :: FRECHET2:16
for T being non empty TopStruct
for S being sequence of T
for S1 being subsequence of S holds Lim S c= Lim S1
proofend;

theorem Th17: :: FRECHET2:17
for T being non empty TopStruct holds Cl_Seq ({} T) = {}
proofend;

theorem Th18: :: FRECHET2:18
for T being non empty TopStruct
for A being Subset of T holds A c= Cl_Seq A
proofend;

theorem Th19: :: FRECHET2:19
for T being non empty TopStruct
for A, B being Subset of T holds (Cl_Seq A) \/ (Cl_Seq B) = Cl_Seq (A \/ B)
proofend;

theorem Th20: :: FRECHET2:20
for T being non empty TopStruct holds
( T is Frechet iff for A being Subset of T holds Cl A = Cl_Seq A )
proofend;

theorem Th21: :: FRECHET2:21
for T being non empty TopSpace st T is Frechet holds
for A, B being Subset of T holds
( Cl_Seq ({} T) = {} &amp; A c= Cl_Seq A &amp; Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) &amp; Cl_Seq (Cl_Seq A) = Cl_Seq A )
proofend;

theorem Th22: :: FRECHET2:22
for T being non empty TopSpace st T is sequential &amp; ( for A being Subset of T holds Cl_Seq (Cl_Seq A) = Cl_Seq A ) holds
T is Frechet
proofend;

theorem :: FRECHET2:23
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) = {} &amp; A c= Cl_Seq A &amp; Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) &amp; Cl_Seq (Cl_Seq A) = Cl_Seq A ) ) by Th21, Th22;

begin

definition
let T be non empty TopSpace;
let S be sequence of T;
assume A1: ex x being Point of T st Lim S = {x} ;
func lim S ->  Point of T means :Def2: :: FRECHET2:def 2
S is_convergent_to it;
existence
 ex b1 being Point of T st S is_convergent_to b1
proofend;
uniqueness
 for b1, b2 being Point of T st S is_convergent_to b1 &amp; S is_convergent_to b2 holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines lim FRECHET2:def_2_:_
 for T being non empty TopSpace
for S being sequence of T st ex x being Point of T st Lim S = {x} holds
for b3 being Point of T holds
( b3 = lim S iff S is_convergent_to b3 );

theorem Th24: :: FRECHET2:24
for T being non empty TopSpace st T is T_2 holds
for S being sequence of T st S is convergent holds
ex x being Point of T st Lim S = {x}
proofend;

theorem Th25: :: FRECHET2:25
for T being non empty TopSpace st T is T_2 holds
for S being sequence of T
for x being Point of T holds
( S is_convergent_to x iff ( S is convergent &amp; x = lim S ) )
proofend;

theorem :: FRECHET2:26
for M being MetrStruct
for S being sequence of M holds S is sequence of (TopSpaceMetr M)
proofend;

theorem :: FRECHET2:27
for M being non empty MetrStruct
for S being sequence of (TopSpaceMetr M) holds S is sequence of M by TOPMETR:12;

theorem Th28: :: FRECHET2:28
for M being non empty MetrSpace
for S being sequence of M
for x being Point of M
for S9 being sequence of (TopSpaceMetr M)
for x9 being Point of (TopSpaceMetr M) st S = S9 &amp; x = x9 holds
( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 )
proofend;

theorem :: FRECHET2:29
for M being non empty MetrSpace
for Sm being sequence of M
for St being sequence of (TopSpaceMetr M) st Sm = St holds
( Sm is convergent iff St is convergent )
proofend;

theorem :: FRECHET2:30
for M being non empty MetrSpace
for Sm being sequence of M
for St being sequence of (TopSpaceMetr M) st Sm = St &amp; Sm is convergent holds
lim Sm = lim St
proofend;

begin

definition
let T be TopStruct ;
let S be sequence of T;
let x be Point of T;
predx is_a_cluster_point_of S means :Def3: :: FRECHET2:def 3
 for O being Subset of T
for n being Element of NAT st O is open &amp; x in O holds
ex m being Element of NAT st
( n <= m &amp; S . m in O );
end;

:: deftheorem Def3 defines is_a_cluster_point_of FRECHET2:def_3_:_
 for T being TopStruct
for S being sequence of T
for x being Point of T holds
( x is_a_cluster_point_of S iff for O being Subset of T
for n being Element of NAT st O is open &amp; x in O holds
ex m being Element of NAT st
( n <= m &amp; S . m in O ) );

theorem Th31: :: FRECHET2:31
for T being non empty TopStruct
for S being sequence of T
for 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
proofend;

theorem :: FRECHET2:32
for T being non empty TopStruct
for S being sequence of T
for x being Point of T st S is_convergent_to x holds
x is_a_cluster_point_of S
proofend;

theorem Th33: :: FRECHET2:33
for T being non empty TopStruct
for S being sequence of T
for x being Point of T
for Y being Subset of T st Y =  {  y where y is Point of T : x in Cl {y}  }  &amp; rng S c= Y holds
S is_convergent_to x
proofend;

theorem Th34: :: FRECHET2:34
for T being non empty TopStruct
for S being sequence of T
for x, y being Point of T st ( for n being Element of NAT holds
( S . n = y &amp; S is_convergent_to x ) ) holds
x in Cl {y}
proofend;

theorem Th35: :: FRECHET2:35
for T being non empty TopStruct
for x being Point of T
for Y being Subset of T
for S being sequence of T st Y =  {  y where y is Point of T : x in Cl {y}  }  &amp; rng S misses Y &amp; S is_convergent_to x holds
ex S1 being subsequence of S st S1 is one-to-one
proofend;

theorem Th36: :: FRECHET2:36
for T being non empty TopStruct
for S1, S2 being sequence of T st rng S2 c= rng S1 &amp; S2 is one-to-one holds
ex P being Permutation of NAT st S2 * P is subsequence of S1
proofend;

scheme :: FRECHET2:sch 1
PermSeq{ F1() ->  non empty 1-sorted , F2() ->  sequence of F1(), F3() ->  Permutation of NAT, P1[ set ] } :
 ex n being Element of NAT st
for m being Element of NAT st n <= m holds
P1[(F2() * F3()) . m]
provided
A1: ex n being Element of NAT st
for m being Element of NAT
for x being Point of F1() st n <= m &amp; x = F2() . m holds
P1[x]
proofend;

scheme :: FRECHET2:sch 2
PermSeq2{ F1() ->  non empty TopStruct , F2() ->  sequence of F1(), F3() ->  Permutation of NAT, P1[ set ] } :
 ex n being Element of NAT st
for m being Element of NAT st n <= m holds
P1[(F2() * F3()) . m]
provided
A1: ex n being Element of NAT st
for m being Element of NAT
for x being Point of F1() st n <= m &amp; x = F2() . m holds
P1[x]
proofend;

theorem Th37: :: FRECHET2:37
for T being non empty TopStruct
for S being sequence of T
for P being Permutation of NAT
for x being Point of T st S is_convergent_to x holds
S * P is_convergent_to x
proofend;

theorem :: FRECHET2:38
for n0 being Element of NAT ex NS being increasing sequence of NAT st
for n being Element of NAT holds NS . n = n + n0
proofend;

theorem Th39: :: FRECHET2:39
for T being non empty TopStruct
for S being sequence of T
for x being Point of T
for n0 being Nat st x is_a_cluster_point_of S holds
x is_a_cluster_point_of S ^\ n0
proofend;

theorem Th40: :: FRECHET2:40
for T being non empty TopStruct
for S being sequence of T
for x being Point of T st x is_a_cluster_point_of S holds
x in Cl (rng S)
proofend;

theorem :: FRECHET2:41
for T being non empty TopStruct st T is Frechet holds
for S being sequence of T
for 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
proofend;

begin

theorem :: FRECHET2:42
for T being non empty TopSpace st T is first-countable holds
for x being Point of T ex B being Basis of x ex S being Function st
( dom S = NAT &amp; rng S = B &amp; ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) ) by Lm5;

theorem :: FRECHET2:43
for T being non empty TopSpace st ( for p being Point of T holds Cl {p} = {p} ) holds
T is T_1 by Lm1;

theorem :: FRECHET2:44
for T being non empty TopSpace st T is T_2 holds
T is T_1 by Lm4;

theorem :: FRECHET2:45
for T being non empty TopSpace st not T is T_1 holds
ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 &amp; x1 <> x2 &amp; S is_convergent_to x2 ) by Lm3;