:: First-countable, Sequential, and { F } rechet Spaces
:: by Bart{\l}omiej Skorulski
::
:: Received May 13, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

Lm1: for r being Real st r > 0 holds
ex n being Element of NAT st
( 1 / n < r & n > 0 )

proof end;

::
:: Preliminaries
::
theorem :: FRECHET:1
for T being non empty 1-sorted
for S being sequence of T holds rng S is Subset of T ;

theorem Th2: :: FRECHET:2
for T1 being non empty 1-sorted
for T2 being 1-sorted
for S being sequence of T1 st rng S c= the carrier of T2 holds
S is sequence of T2
proof end;

theorem Th3: :: FRECHET:3
for T being non empty TopSpace
for x being Point of T
for B being Basis of x holds B <> {}
proof end;

registration
let T be non empty TopSpace;
let x be Point of T;
cluster open x -quasi_basis -> non empty for Element of K19(K19( the carrier of T));
coherence
for b1 being Basis of x holds not b1 is empty
by Th3;
end;

Lm2: for T being TopStruct
for A being Subset of T holds
( A is open iff ([#] T) \ A is closed )

proof end;

theorem Th4: :: FRECHET:4
for T being TopSpace
for A, B being Subset of T st A is open & B is closed holds
A \ B is open
proof end;

theorem Th5: :: FRECHET:5
for T being TopStruct st {} T is closed & [#] T is closed & ( for A, B being Subset of T st A is closed & B is closed holds
A \/ B is closed ) & ( for F being Subset-Family of T st F is closed holds
meet F is closed ) holds
T is TopSpace
proof end;

theorem Th6: :: FRECHET:6
for T being TopSpace
for S being non empty TopStruct
for f being Function of T,S st ( for A being Subset of S holds
( A is closed iff f " A is closed ) ) holds
S is TopSpace
proof end;

theorem Th7: :: FRECHET:7
for x being Point of RealSpace
for r being Real holds Ball (x,r) = ].(x - r),(x + r).[
proof end;

theorem :: FRECHET:8
for A being Subset of R^1 holds
( A is open iff for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) )
proof end;

theorem Th9: :: FRECHET:9
for S being sequence of R^1 st ( for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ ) holds
rng S is closed
proof end;

theorem Th10: :: FRECHET:10
for B being Subset of R^1 st B = NAT holds
B is closed
proof end;

definition
let M be non empty MetrStruct ;
let x be Point of (TopSpaceMetr M);
func Balls x -> Subset-Family of (TopSpaceMetr M) means :Def1: :: FRECHET:def 1
ex y being Point of M st
( y = x & it = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } );
existence
ex b1 being Subset-Family of (TopSpaceMetr M) ex y being Point of M st
( y = x & b1 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } )
proof end;
uniqueness
for b1, b2 being Subset-Family of (TopSpaceMetr M) st ex y being Point of M st
( y = x & b1 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) & ex y being Point of M st
( y = x & b2 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) holds
b1 = b2
;
end;

:: deftheorem Def1 defines Balls FRECHET:def 1 :
for M being non empty MetrStruct
for x being Point of (TopSpaceMetr M)
for b3 being Subset-Family of (TopSpaceMetr M) holds
( b3 = Balls x iff ex y being Point of M st
( y = x & b3 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) );

registration
let M be non empty MetrSpace;
let x be Point of (TopSpaceMetr M);
cluster Balls x -> open x -quasi_basis ;
coherence
( Balls x is open & Balls x is x -quasi_basis )
proof end;
end;

registration
let M be non empty MetrSpace;
let x be Point of (TopSpaceMetr M);
cluster Balls x -> countable ;
coherence
Balls x is countable
proof end;
end;

theorem Th11: :: FRECHET:11
for M being non empty MetrSpace
for x being Point of (TopSpaceMetr M)
for x9 being Point of M st x = x9 holds
ex f being Function of NAT,(Balls x) st
for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))
proof end;

theorem Th12: :: FRECHET:12
for f, g being Function holds rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g)
proof end;

theorem Th13: :: FRECHET:13
for A, B being set st B c= A holds
(id A) .: B = B
proof end;

theorem Th14: :: FRECHET:14
for A, B, x being set holds dom ((id A) +* (B --> x)) = A \/ B
proof end;

theorem Th15: :: FRECHET:15
for A, B, x being set st B <> {} holds
rng ((id A) +* (B --> x)) = (A \ B) \/ {x}
proof end;

theorem Th16: :: FRECHET:16
for A, B, C, x being set st C c= A holds
((id A) +* (B --> x)) " (C \ {x}) = (C \ B) \ {x}
proof end;

theorem Th17: :: FRECHET:17
for A, B, x being set st not x in A holds
((id A) +* (B --> x)) " {x} = B
proof end;

theorem Th18: :: FRECHET:18
for A, B, C, x being set st C c= A & not x in A holds
((id A) +* (B --> x)) " (C \/ {x}) = C \/ B
proof end;

theorem Th19: :: FRECHET:19
for A, B, C, x being set st C c= A & not x in A holds
((id A) +* (B --> x)) " (C \ {x}) = C \ B
proof end;

begin

::
:: Convergent Sequences in Topological Spaces,
:: FIRST-COUNTABLE, SEQUENTIAL, FRECHET SPACES
::
definition
let T be non empty TopStruct ;
attr T is first-countable means :Def2: :: FRECHET:def 2
for x being Point of T ex B being Basis of x st B is countable ;
end;

:: deftheorem Def2 defines first-countable FRECHET:def 2 :
for T being non empty TopStruct holds
( T is first-countable iff for x being Point of T ex B being Basis of x st B is countable );

theorem Th20: :: FRECHET:20
for M being non empty MetrSpace holds TopSpaceMetr M is first-countable
proof end;

theorem :: FRECHET:21
R^1 is first-countable by Th20;

registration
cluster R^1 -> first-countable ;
coherence
R^1 is first-countable
by Th20;
end;

definition
let T be TopStruct ;
let S be sequence of T;
let x be Point of T;
pred S is_convergent_to x means :Def3: :: FRECHET:def 3
for U1 being Subset of T st U1 is open & x in U1 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1;
end;

:: deftheorem Def3 defines is_convergent_to FRECHET:def 3 :
for T being TopStruct
for S being sequence of T
for x being Point of T holds
( S is_convergent_to x iff for U1 being Subset of T st U1 is open & x in U1 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S . m in U1 );

theorem Th22: :: FRECHET:22
for T being non empty TopStruct
for x being Point of T
for S being sequence of T st S = NAT --> x holds
S is_convergent_to x
proof end;

definition
let T be TopStruct ;
let S be sequence of T;
attr S is convergent means :Def4: :: FRECHET:def 4
ex x being Point of T st S is_convergent_to x;
end;

:: deftheorem Def4 defines convergent FRECHET:def 4 :
for T being TopStruct
for S being sequence of T holds
( S is convergent iff ex x being Point of T st S is_convergent_to x );

definition
let T be non empty TopStruct ;
let S be sequence of T;
func Lim S -> Subset of T means :Def5: :: FRECHET:def 5
for x being Point of T holds
( x in it iff S is_convergent_to x );
existence
ex b1 being Subset of T st
for x being Point of T holds
( x in b1 iff S is_convergent_to x )
proof end;
uniqueness
for b1, b2 being Subset of T st ( for x being Point of T holds
( x in b1 iff S is_convergent_to x ) ) & ( for x being Point of T holds
( x in b2 iff S is_convergent_to x ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Lim FRECHET:def 5 :
for T being non empty TopStruct
for S being sequence of T
for b3 being Subset of T holds
( b3 = Lim S iff for x being Point of T holds
( x in b3 iff S is_convergent_to x ) );

definition
let T be non empty TopStruct ;
attr T is Frechet means :Def6: :: FRECHET:def 6
for A being Subset of T
for x being Point of T st x in Cl A holds
ex S being sequence of T st
( rng S c= A & x in Lim S );
end;

:: deftheorem Def6 defines Frechet FRECHET:def 6 :
for T being non empty TopStruct holds
( T is Frechet iff for A being Subset of T
for x being Point of T st x in Cl A holds
ex S being sequence of T st
( rng S c= A & x in Lim S ) );

definition
let T be non empty TopStruct ;
attr T is sequential means :: FRECHET:def 7
for A being Subset of T holds
( A is closed iff for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A );
end;

:: deftheorem defines sequential FRECHET:def 7 :
for T being non empty TopStruct holds
( T is sequential iff for A being Subset of T holds
( A is closed iff for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) );

theorem Th23: :: FRECHET:23
for T being non empty TopSpace st T is first-countable holds
T is Frechet
proof end;

registration
cluster non empty TopSpace-like first-countable -> non empty Frechet for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is first-countable holds
b1 is Frechet
by Th23;
end;

theorem Th24: :: FRECHET:24
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
proof end;

theorem Th25: :: FRECHET:25
for T being non empty TopSpace st ( for A being Subset of T st ( for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) holds
A is closed ) holds
T is sequential
proof end;

theorem Th26: :: FRECHET:26
for T being non empty TopSpace st T is Frechet holds
T is sequential
proof end;

registration
cluster non empty TopSpace-like Frechet -> non empty sequential for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is Frechet holds
b1 is sequential
by Th26;
end;

begin

::
:: Not (for T holds T is Frechet implies T is first-countable)
::
definition
func REAL? -> non empty strict TopSpace means :Def8: :: FRECHET:def 8
( the carrier of it = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,it st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of it holds
( A is closed iff f " A is closed ) ) ) );
existence
ex b1 being non empty strict TopSpace st
( the carrier of b1 = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b1 st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b1 holds
( A is closed iff f " A is closed ) ) ) )
proof end;
uniqueness
for b1, b2 being non empty strict TopSpace st the carrier of b1 = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b1 st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b1 holds
( A is closed iff f " A is closed ) ) ) & the carrier of b2 = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b2 st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b2 holds
( A is closed iff f " A is closed ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines REAL? FRECHET:def 8 :
for b1 being non empty strict TopSpace holds
( b1 = REAL? iff ( the carrier of b1 = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b1 st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b1 holds
( A is closed iff f " A is closed ) ) ) ) );

Lm3: {REAL} c= the carrier of REAL?
proof end;

theorem Th27: :: FRECHET:27
REAL is Point of REAL?
proof end;

theorem Th28: :: FRECHET:28
for A being Subset of REAL? holds
( ( A is open & REAL in A ) iff ex O being Subset of R^1 st
( O is open & NAT c= O & A = (O \ NAT) \/ {REAL} ) )
proof end;

theorem Th29: :: FRECHET:29
for A being set holds
( A is Subset of REAL? & not REAL in A iff ( A is Subset of R^1 & NAT /\ A = {} ) )
proof end;

theorem Th30: :: FRECHET:30
for A being Subset of R^1
for B being Subset of REAL? st A = B holds
( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) )
proof end;

theorem Th31: :: FRECHET:31
for A being Subset of REAL? st A = {REAL} holds
A is closed
proof end;

theorem Th32: :: FRECHET:32
not REAL? is first-countable
proof end;

theorem Th33: :: FRECHET:33
REAL? is Frechet
proof end;

theorem :: FRECHET:34
ex T being non empty TopSpace st
( T is Frechet & not T is first-countable ) by Th32, Th33;

begin

::
:: Auxiliary theorems
::
::Moved from CIRCCMB2:5, AK, 20.02.2006
theorem :: FRECHET:35
for f, g being Function st f tolerates g holds
rng (f +* g) = (rng f) \/ (rng g)
proof end;

theorem :: FRECHET:36
for r being Real st r > 0 holds
ex n being Element of NAT st
( 1 / n < r & n > 0 ) by Lm1;