:: FRECHET semantic presentation

Lm1: for n being Nat st n <> 0 holds
1 / n > 0

proof end;

Lm2: for r being Real st r > 0 holds
ex n being Nat st
( 1 / n < r & n > 0 )

proof end;

theorem Th1: :: FRECHET:1

for T being non empty 1-sorted
for S being sequence of T holds rng S is Subset of T

proof end;

definition

let T be non empty 1-sorted ;
let S be sequence of T;
:: original: rng
redefine func rng S -> Subset of T;
coherence by Th1;

end;

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 -> non empty Basis of x;
coherence by Th3;

end;

Lm3: 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 x', r being Real st x' = x & r > 0 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 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;

theorem Th11: :: FRECHET:11

for M being non empty MetrSpace
for x being Point of (TopSpaceMetr M)
for x' being Point of M st x = x' holds
ex B being Basis of x st
( B = { (Ball x',(1 / n)) where n is Nat : n <> 0 } & B is countable & ex f being Function of NAT ,B st
for n being set st n in NAT holds
ex n' being Nat st
( n = n' & f . n = Ball x',(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 :: FRECHET:14

canceled;

theorem Th15: :: FRECHET:15

for A, B, x being set holds dom ((id A) +* (B --> x)) = A \/ B

proof end;

theorem Th16: :: FRECHET:16

for A, B, x being set st B <> {} holds
rng ((id A) +* (B --> x)) = (A \ B) \/ {x}

proof end;

theorem Th17: :: FRECHET:17

for A, B, C, x being set st C c= A holds
((id A) +* (B --> x)) " (C \ {x}) = (C \ B) \ {x}

proof end;

theorem Th18: :: FRECHET:18

for A, B, x being set st not x in A holds
((id A) +* (B --> x)) " {x} = 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;

theorem Th20: :: FRECHET:20

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;

Lm4: for A, B, C, x being set st not x in A holds
((id A) +* (B --> x)) " ((A \ C) \ {x}) = (A \ C) \ B

proof end;

definition

let T be non empty TopStruct ;
attr T is first-countable means :Def1: :: FRECHET:def 1
for x being Point of T ex B being Basis of x st B is countable;

end;

:: deftheorem Def1 defines first-countable FRECHET:def 1 :

theorem Th21: :: FRECHET:21

for M being non empty MetrSpace holds TopSpaceMetr M is first-countable

proof end;

theorem :: FRECHET:22

R^1 is first-countable by Th21, TOPMETR:def 7;

registration

cluster R^1 -> first-countable ;
coherence by Th21, TOPMETR:def 7;

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 :Def2: :: FRECHET:def 2
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 Def2 defines is_convergent_to FRECHET:def 2 :

theorem Th23: :: FRECHET:23

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 :Def3: :: FRECHET:def 3
ex x being Point of T st S is_convergent_to x;

end;

:: deftheorem Def3 defines convergent FRECHET:def 3 :

definition

let T be non empty TopStruct ;
let S be sequence of T;
func Lim S -> Subset of T means :Def4: :: FRECHET:def 4
for x being Point of T holds
( x in it iff S is_convergent_to x );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Lim FRECHET:def 4 :

definition

let T be non empty TopStruct ;
attr T is Frechet means :Def5: :: FRECHET:def 5
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 Def5 defines Frechet FRECHET:def 5 :

definition

let T be non empty TopStruct ;
attr T is sequential means :: FRECHET:def 6
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 6 :

theorem Th24: :: FRECHET:24

for T being non empty TopSpace st T is first-countable holds
T is Frechet

proof end;

registration

cluster non empty first-countable -> non empty Frechet TopStruct ;
coherence by Th24;

end;

theorem :: FRECHET:25

canceled;

theorem Th26: :: FRECHET:26

for T being non empty TopSpace
for A being Subset of T st A is closed holds
for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A

proof end;

theorem Th27: :: FRECHET:27

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 Th28: :: FRECHET:28

for T being non empty TopSpace st T is Frechet holds
T is sequential

proof end;

registration

cluster non empty Frechet -> non empty sequential TopStruct ;
coherence by Th28;

end;

definition

func REAL? -> non empty strict TopSpace means :Def7: :: FRECHET:def 7
( 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines REAL? FRECHET:def 7 :

Lm5: {REAL } c= the carrier of REAL?

proof end;

theorem :: FRECHET:29

canceled;

theorem Th30: :: FRECHET:30

REAL is Point of REAL?

proof end;

theorem Th31: :: FRECHET:31

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 Th32: :: FRECHET:32

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 Th33: :: FRECHET:33

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

for A being Subset of REAL? st A = {REAL } holds
A is closed

proof end;

theorem Th35: :: FRECHET:35

not REAL? is first-countable

proof end;

theorem Th36: :: FRECHET:36

REAL? is Frechet

proof end;

theorem :: FRECHET:37

ex T being non empty TopSpace st
( T is Frechet & not T is first-countable ) by Th35, Th36;

theorem :: FRECHET:38

canceled;

theorem :: FRECHET:39

canceled;

theorem :: FRECHET:40

for r being Real st r > 0 holds
ex n being Nat st
( 1 / n < r & n > 0 ) by Lm2;