:: by Bart{\l}omiej Skorulski

::

:: Received May 13, 1998

:: Copyright (c) 1998-2019 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;

theorem :: FRECHET:1

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

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;

registration

let T be non empty TopSpace;

let x be Point of T;

coherence

for b_{1} being Basis of x holds not b_{1} is empty
by Th3;

end;
let x be Point of T;

coherence

for b

Lm2: for T being TopStruct

for A being Subset of T holds

( A is open iff ([#] T) \ A is closed )

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

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

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 :: 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 ) )

( 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

rng S is closed

proof end;

definition

let M be non empty MetrStruct ;

let x be Point of (TopSpaceMetr M);

ex b_{1} being Subset-Family of (TopSpaceMetr M) ex y being Point of M st

( y = x & b_{1} = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } )

for b_{1}, b_{2} being Subset-Family of (TopSpaceMetr M) st ex y being Point of M st

( y = x & b_{1} = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } ) & ex y being Point of M st

( y = x & b_{2} = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } ) holds

b_{1} = b_{2}
;

end;
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 y being Point of M st

( y = x & it = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } );

ex b

( y = x & b

proof end;

uniqueness for b

( y = x & b

( y = x & b

b

:: deftheorem Def1 defines Balls FRECHET:def 1 :

for M being non empty MetrStruct

for x being Point of (TopSpaceMetr M)

for b_{3} being Subset-Family of (TopSpaceMetr M) holds

( b_{3} = Balls x iff ex y being Point of M st

( y = x & b_{3} = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } ) );

for M being non empty MetrStruct

for x being Point of (TopSpaceMetr M)

for b

( b

( y = x & b

registration

let M be non empty MetrSpace;

let x be Point of (TopSpaceMetr M);

coherence

( Balls x is open & Balls x is x -quasi_basis )

end;
let x be Point of (TopSpaceMetr M);

coherence

( Balls x is open & Balls x is x -quasi_basis )

proof end;

registration

let M be non empty MetrSpace;

let x be Point of (TopSpaceMetr M);

coherence

Balls x is countable

end;
let x be Point of (TopSpaceMetr M);

coherence

Balls x is countable

proof 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)))

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;

::

:: Convergent Sequences in Topological Spaces,

:: FIRST-COUNTABLE, SEQUENTIAL, FRECHET SPACES

::

:: Convergent Sequences in Topological Spaces,

:: FIRST-COUNTABLE, SEQUENTIAL, FRECHET SPACES

::

definition

let T be non empty TopStruct ;

end;
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 ;

for x being Point of T ex B being Basis of x st B is countable ;

:: 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 );

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 );

:: 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 );

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

for x being Point of T

for S being sequence of T st S = NAT --> x holds

S is_convergent_to x

proof 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 );

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;

ex b_{1} being Subset of T st

for x being Point of T holds

( x in b_{1} iff S is_convergent_to x )

for b_{1}, b_{2} being Subset of T st ( for x being Point of T holds

( x in b_{1} iff S is_convergent_to x ) ) & ( for x being Point of T holds

( x in b_{2} iff S is_convergent_to x ) ) holds

b_{1} = b_{2}

end;
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 for x being Point of T holds

( x in it iff S is_convergent_to x );

ex b

for x being Point of T holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def5 defines Lim FRECHET:def 5 :

for T being non empty TopStruct

for S being sequence of T

for b_{3} being Subset of T holds

( b_{3} = Lim S iff for x being Point of T holds

( x in b_{3} iff S is_convergent_to x ) );

for T being non empty TopStruct

for S being sequence of T

for b

( b

( x in b

:: 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 ) );

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 ;

end;
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 );

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 );

:: 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 ) );

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 ) );

registration

coherence

for b_{1} being non empty TopSpace st b_{1} is first-countable holds

b_{1} is Frechet
by Th23;

end;
for b

b

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

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;

registration
end;

::

:: Not (for T holds T is Frechet implies T is first-countable)

::

:: Not (for T holds T is Frechet implies T is first-countable)

::

definition

ex b_{1} being non empty strict TopSpace st

( the carrier of b_{1} = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b_{1} st

( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b_{1} holds

( A is closed iff f " A is closed ) ) ) )

for b_{1}, b_{2} being non empty strict TopSpace st the carrier of b_{1} = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b_{1} st

( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b_{1} holds

( A is closed iff f " A is closed ) ) ) & the carrier of b_{2} = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b_{2} st

( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b_{2} holds

( A is closed iff f " A is closed ) ) ) holds

b_{1} = b_{2}
end;

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 ( 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 ) ) ) );

ex b

( the carrier of b

( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b

( A is closed iff f " A is closed ) ) ) )

proof end;

uniqueness for b

( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b

( A is closed iff f " A is closed ) ) ) & the carrier of b

( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b

( A is closed iff f " A is closed ) ) ) holds

b

proof end;

:: deftheorem Def8 defines REAL? FRECHET:def 8 :

for b_{1} being non empty strict TopSpace holds

( b_{1} = REAL? iff ( the carrier of b_{1} = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b_{1} st

( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b_{1} holds

( A is closed iff f " A is closed ) ) ) ) );

for b

( b

( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b

( A is closed iff f " A is closed ) ) ) ) );

Lm3: {REAL} c= the carrier 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} ) )

( ( 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 = {} ) )

( 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 ) )

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 :: FRECHET:34

::

:: Auxiliary theorems

::

::Moved from CIRCCMB2:5, AK, 20.02.2006

:: Auxiliary theorems

::

::Moved from CIRCCMB2:5, AK, 20.02.2006

theorem :: FRECHET:36

:: Preliminaries

::