:: FRECHET semantic presentation

Lemma1: for b₁ being Nat st b₁ <> 0 holds
1 / b₁ > 0

proof end;

Lemma2: for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
( 1 / b₂ < b₁ & b₂ > 0 )

proof end;

theorem Th1: :: FRECHET:1

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁ holds rng b₂ is Subset of b₁

proof end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be sequence of c₁;
redefine func rng as rng c₂ -> Subset of a₁;
coherence by Th1;

end;

theorem Th2: :: FRECHET:2

for b₁ being non empty 1-sorted
for b₂ being 1-sorted
for b₃ being sequence of b₁ st rng b₃ c= the carrier of b₂ holds
b₃ is sequence of b₂

proof end;

theorem Th3: :: FRECHET:3

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Basis of b₂ holds b₃ <> {}

proof end;

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
cluster -> non empty Basis of a₂;
coherence by Th3;

end;

Lemma6: for b₁ being TopStruct
for b₂ being Subset of b₁ holds
( b₂ is open iff ([#] b₁) \ b₂ is closed )

proof end;

theorem Th4: :: FRECHET:4

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is open & b₃ is closed holds
b₂ \ b₃ is open

proof end;

theorem Th5: :: FRECHET:5

for b₁ being TopStruct st {} b₁ is closed & [#] b₁ is closed & ( for b₂, b₃ being Subset of b₁ st b₂ is closed & b₃ is closed holds
b₂ \/ b₃ is closed ) & ( for b₂ being Subset-Family of b₁ st b₂ is closed holds
meet b₂ is closed ) holds
b₁ is TopSpace

proof end;

theorem Th6: :: FRECHET:6

for b₁ being TopSpace
for b₂ being non empty TopStruct
for b₃ being Function of b₁,b₂ st ( for b₄ being Subset of b₂ holds
( b₄ is closed iff b₃ " b₄ is closed ) ) holds
b₂ is TopSpace

proof end;

theorem Th7: :: FRECHET:7

for b₁ being Point of RealSpace
for b₂, b₃ being Real st b₂ = b₁ & b₃ > 0 holds
Ball b₁,b₃ = ].(b₂ - b₃),(b₂ + b₃).[

proof end;

theorem Th8: :: FRECHET:8

for b₁ being Subset of R^1 holds
( b₁ is open iff for b₂ being Real st b₂ in b₁ holds
ex b₃ being Real st
( b₃ > 0 & ].(b₂ - b₃),(b₂ + b₃).[ c= b₁ ) )

proof end;

theorem Th9: :: FRECHET:9

for b₁ being sequence of R^1 st ( for b₂ being Nat holds b₁ . b₂ in ].(b₂ - (1 / 4)),(b₂ + (1 / 4)).[ ) holds
rng b₁ 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 b₁ being non empty MetrSpace
for b₂ being Point of (TopSpaceMetr b₁)
for b₃ being Point of b₁ st b₂ = b₃ holds
ex b₄ being Basis of b₂ st
( b₄ = { (Ball b₃,(1 / b₅)) where B is Nat : b₅ <> 0 } & b₄ is countable & ex b₅ being Function of NAT ,b₄ st
for b₆ being set st b₆ in NAT holds
ex b₇ being Nat st
( b₆ = b₇ & b₅ . b₆ = Ball b₃,(1 / (b₇ + 1)) ) )

proof end;

theorem Th12: :: FRECHET:12

for b₁, b₂ being Function holds rng (b₁ +* b₂) = (b₁ .: ((dom b₁) \ (dom b₂))) \/ (rng b₂)

proof end;

theorem Th13: :: FRECHET:13

for b₁, b₂ being set st b₂ c= b₁ holds
(id b₁) .: b₂ = b₂

proof end;

theorem Th14: :: FRECHET:14

canceled;

theorem Th15: :: FRECHET:15

for b₁, b₂, b₃ being set holds dom ((id b₁) +* (b₂ --> b₃)) = b₁ \/ b₂

proof end;

theorem Th16: :: FRECHET:16

for b₁, b₂, b₃ being set st b₂ <> {} holds
rng ((id b₁) +* (b₂ --> b₃)) = (b₁ \ b₂) \/ {b₃}

proof end;

theorem Th17: :: FRECHET:17

for b₁, b₂, b₃, b₄ being set st b₃ c= b₁ holds
((id b₁) +* (b₂ --> b₄)) " (b₃ \ {b₄}) = (b₃ \ b₂) \ {b₄}

proof end;

theorem Th18: :: FRECHET:18

for b₁, b₂, b₃ being set st not b₃ in b₁ holds
((id b₁) +* (b₂ --> b₃)) " {b₃} = b₂

proof end;

theorem Th19: :: FRECHET:19

for b₁, b₂, b₃, b₄ being set st b₃ c= b₁ & not b₄ in b₁ holds
((id b₁) +* (b₂ --> b₄)) " (b₃ \/ {b₄}) = b₃ \/ b₂

proof end;

theorem Th20: :: FRECHET:20

for b₁, b₂, b₃, b₄ being set st b₃ c= b₁ & not b₄ in b₁ holds
((id b₁) +* (b₂ --> b₄)) " (b₃ \ {b₄}) = b₃ \ b₂

proof end;

Lemma22: for b₁, b₂, b₃, b₄ being set st not b₄ in b₁ holds
((id b₁) +* (b₂ --> b₄)) " ((b₁ \ b₃) \ {b₄}) = (b₁ \ b₃) \ b₂

proof end;

definition

let c₁ be non empty TopStruct ;
attr a₁ is first-countable means :Def1: :: FRECHET:def 1
for b₁ being Point of a₁ ex b₂ being Basis of b₁ st b₂ is countable;

end;

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

theorem Th21: :: FRECHET:21

for b₁ being non empty MetrSpace holds TopSpaceMetr b₁ is first-countable

proof end;

theorem Th22: :: 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 c₁ be TopStruct ;
let c₂ be sequence of c₁;
let c₃ be Point of c₁;
pred c₂ is_convergent_to c₃ means :Def2: :: FRECHET:def 2
for b₁ being Subset of a₁ st b₁ is open & a₃ in b₁ holds
ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
a₂ . b₃ in b₁;

end;

:: deftheorem Def2 defines is_convergent_to FRECHET:def 2 :

theorem Th23: :: FRECHET:23

for b₁ being non empty TopStruct
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ = NAT --> b₂ holds
b₃ is_convergent_to b₂

proof end;

definition

let c₁ be TopStruct ;
let c₂ be sequence of c₁;
attr a₂ is convergent means :Def3: :: FRECHET:def 3
ex b₁ being Point of a₁ st a₂ is_convergent_to b₁;

end;

:: deftheorem Def3 defines convergent FRECHET:def 3 :

definition

let c₁ be non empty TopStruct ;
let c₂ be sequence of c₁;
func Lim c₂ -> Subset of a₁ means :Def4: :: FRECHET:def 4
for b₁ being Point of a₁ holds
( b₁ in a₃ iff a₂ is_convergent_to b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Lim FRECHET:def 4 :

definition

let c₁ be non empty TopStruct ;
attr a₁ is Frechet means :Def5: :: FRECHET:def 5
for b₁ being Subset of a₁
for b₂ being Point of a₁ st b₂ in Cl b₁ holds
ex b₃ being sequence of a₁ st
( rng b₃ c= b₁ & b₂ in Lim b₃ );

end;

:: deftheorem Def5 defines Frechet FRECHET:def 5 :

definition

let c₁ be non empty TopStruct ;
attr a₁ is sequential means :: FRECHET:def 6
for b₁ being Subset of a₁ holds
( b₁ is closed iff for b₂ being sequence of a₁ st b₂ is convergent & rng b₂ c= b₁ holds
Lim b₂ c= b₁ );

end;

:: deftheorem Def6 defines sequential FRECHET:def 6 :

theorem Th24: :: FRECHET:24

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

proof end;

registration

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

end;

theorem Th25: :: FRECHET:25

canceled;

theorem Th26: :: FRECHET:26

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is closed holds
for b₃ being sequence of b₁ st b₃ is convergent & rng b₃ c= b₂ holds
Lim b₃ c= b₂

proof end;

theorem Th27: :: FRECHET:27

for b₁ being non empty TopSpace st ( for b₂ being Subset of b₁ st ( for b₃ being sequence of b₁ st b₃ is convergent & rng b₃ c= b₂ holds
Lim b₃ c= b₂ ) holds
b₂ is closed ) holds
b₁ is sequential

proof end;

theorem Th28: :: FRECHET:28

for b₁ being non empty TopSpace st b₁ is Frechet holds
b₁ 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 a₁ = (REAL \ NAT ) \/ {REAL } & ex b₁ being Function of R^1 ,a₁ st
( b₁ = (id REAL ) +* (NAT --> REAL ) & ( for b₂ being Subset of a₁ holds
( b₂ is closed iff b₁ " b₂ is closed ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

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

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

proof end;

theorem Th29: :: FRECHET:29

canceled;

theorem Th30: :: FRECHET:30

REAL is Point of REAL?

proof end;

theorem Th31: :: FRECHET:31

for b₁ being Subset of REAL? holds
( ( b₁ is open & REAL in b₁ ) iff ex b₂ being Subset of R^1 st
( b₂ is open & NAT c= b₂ & b₁ = (b₂ \ NAT ) \/ {REAL } ) )

proof end;

theorem Th32: :: FRECHET:32

for b₁ being set holds
( b₁ is Subset of REAL? & not REAL in b₁ iff ( b₁ is Subset of R^1 & NAT /\ b₁ = {} ) )

proof end;

theorem Th33: :: FRECHET:33

for b₁ being Subset of R^1
for b₂ being Subset of REAL? st b₁ = b₂ holds
( NAT /\ b₁ = {} & b₁ is open iff ( not REAL in b₂ & b₂ is open ) )

proof end;

theorem Th34: :: FRECHET:34

for b₁ being Subset of REAL? st b₁ = {REAL } holds
b₁ 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 Th37: :: FRECHET:37

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

theorem Th38: :: FRECHET:38

canceled;

theorem Th39: :: FRECHET:39

canceled;

theorem Th40: :: FRECHET:40

for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
( 1 / b₂ < b₁ & b₂ > 0 ) by Lemma2;