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

Lm1: for r being Real st r > 0 holds
ex n being 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 b₁ being Basis of x holds not b₁ 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 Nat : n <> 0 } );

existence
ex b₁ being Subset-Family of (TopSpaceMetr M) ex y being Point of M st
( y = x & b₁ = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of (TopSpaceMetr M) st ex y being Point of M st
( y = x & b₁ = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } ) & ex y being Point of M st
( y = x & b₂ = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } ) holds
b₁ = b₂ ;

end;

:: deftheorem Def1 defines Balls FRECHET:def 1 :
for M being non empty MetrStruct
for x being Point of (TopSpaceMetr M)
for b₃ being Subset-Family of (TopSpaceMetr M) holds
( b₃ = Balls x iff ex y being Point of M st
( y = x & b₃ = { (Ball (y,(1 / n))) where n is 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 sequence of (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;

::
:: Convergent Sequences in Topological Spaces,
:: FIRST-COUNTABLE, SEQUENTIAL, FRECHET SPACES
::

definition

let T be non empty TopStruct ;

attr T is first-countable means :: FRECHET:def 2
for x being Point of T ex B being Basis of x st B is countable ;

end;

:: deftheorem 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 :: FRECHET:def 3
for U1 being Subset of T st U1 is open & x in U1 holds
ex n being Nat st
for m being Nat st n <= m holds
S . m in U1;

end;

:: deftheorem 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 Nat st
for m being 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 :: FRECHET:def 4
ex x being Point of T st S is_convergent_to x;

end;

:: deftheorem 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 b₁ being Subset of T st
for x being Point of T holds
( x in b₁ iff S is_convergent_to x )

proof end;

uniqueness
for b₁, b₂ being Subset of T st ( for x being Point of T holds
( x in b₁ iff S is_convergent_to x ) ) & ( for x being Point of T holds
( x in b₂ iff S is_convergent_to x ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines Lim FRECHET:def 5 :
for T being non empty TopStruct
for S being sequence of T
for b₃ being Subset of T holds
( b₃ = Lim S iff for x being Point of T holds
( x in b₃ 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 b₁ being non empty TopSpace st b₁ is first-countable holds
b₁ 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 by Th24;

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 b₁ being non empty TopSpace st b₁ is Frechet holds
b₁ is sequential by Th26;

end;

::
:: 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 b₁ being non empty strict TopSpace st
( the carrier of b₁ = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b₁ st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b₁ holds
( A is closed iff f " A is closed ) ) ) )

proof end;

uniqueness
for b₁, b₂ being non empty strict TopSpace st the carrier of b₁ = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b₁ st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b₁ holds
( A is closed iff f " A is closed ) ) ) & the carrier of b₂ = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b₂ st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b₂ holds
( A is closed iff f " A is closed ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines REAL? FRECHET:def 8 :
for b₁ being non empty strict TopSpace holds
( b₁ = REAL? iff ( the carrier of b₁ = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b₁ st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b₁ 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;

::
:: 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 Nat st
( 1 / n < r & n > 0 ) by Lm1;