:: FRECHET2 semantic presentation

Lemma1: for b₁ being non empty TopSpace holds
( b₁ is_T1 iff for b₂ being Point of b₁ holds Cl {b₂} = {b₂} )

proof end;

Lemma2: for b₁ being non empty TopSpace st not b₁ is_T1 holds
ex b₂, b₃ being Point of b₁ st
( b₂ <> b₃ & b₃ in Cl {b₂} )

proof end;

Lemma3: for b₁ being non empty TopSpace st not b₁ is_T1 holds
ex b₂, b₃ being Point of b₁ex b₄ being sequence of b₁ st
( b₄ = NAT --> b₂ & b₂ <> b₃ & b₄ is_convergent_to b₃ )

proof end;

Lemma4: for b₁ being non empty TopSpace st b₁ is_T2 holds
b₁ is_T1

proof end;

Lemma5: for b₁ being non empty 1-sorted
for b₂ being sequence of b₁
for b₃ being Function of NAT , NAT holds b₂ * b₃ is sequence of b₁
;

definition

let c₁ be non empty 1-sorted ;
let c₂ be Function of NAT , NAT ;
let c₃ be sequence of c₁;
redefine func * as c₃ * c₂ -> sequence of a₁;
coherence by Lemma5;

end;

theorem Th1: :: FRECHET2:1

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁
for b₃ being increasing Seq_of_Nat holds b₂ * b₃ is sequence of b₁

proof end;

Lemma7: id NAT is Real_Sequence

proof end;

Lemma8: for b₁ being Real_Sequence st b₁ = id NAT holds
b₁ is natural-yielding

proof end;

Lemma9: for b₁ being Real_Sequence st b₁ = id NAT holds
b₁ is increasing

proof end;

theorem Th2: :: FRECHET2:2

for b₁ being Real_Sequence st b₁ = id NAT holds
b₁ is increasing Seq_of_Nat by Lemma8, Lemma9;

Lemma10: for b₁ being non empty 1-sorted
for b₂ being sequence of b₁ ex b₃ being increasing Seq_of_Nat st b₂ = b₂ * b₃

proof end;

theorem Th3: :: FRECHET2:3

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

proof end;

theorem Th4: :: FRECHET2:4

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁
for b₃ being subsequence of b₂ holds rng b₃ c= rng b₂

proof end;

Lemma13: for b₁ being non empty 1-sorted
for b₂ being sequence of b₁
for b₃ being increasing Seq_of_Nat holds b₂ * b₃ is subsequence of b₂

proof end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be increasing Seq_of_Nat;
let c₃ be sequence of c₁;
redefine func * as c₃ * c₂ -> subsequence of a₃;
correctness by Lemma13;

end;

theorem Th5: :: FRECHET2:5

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁
for b₃ being subsequence of b₂
for b₄ being subsequence of b₃ holds b₄ is subsequence of b₂

proof end;

scheme :: FRECHET2:sch 1
s1{ F₁() -> non empty 1-sorted , F₂() -> sequence of F₁(), P₁[ set ] } :

ex b₁ being subsequence of F₂() st
for b₂ being Nat holds P₁[b₁ . b₂]

provided

E15: for b₁ being Nat ex b₂ being Natex b₃ being Point of F₁() st
( b₁ <= b₂ & b₃ = F₂() . b₂ & P₁[b₃] )

proof end;

scheme :: FRECHET2:sch 2
s2{ F₁() -> non empty TopStruct , F₂() -> sequence of F₁(), P₁[ set ] } :

ex b₁ being subsequence of F₂() st
for b₂ being Nat holds P₁[b₁ . b₂]

provided

E15: for b₁ being Nat ex b₂ being Natex b₃ being Point of F₁() st
( b₁ <= b₂ & b₃ = F₂() . b₂ & P₁[b₃] )

proof end;

theorem Th6: :: FRECHET2:6

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁
for b₃ being Subset of b₁ st ( for b₄ being subsequence of b₂ holds not rng b₄ c= b₃ ) holds
ex b₄ being Nat st
for b₅ being Nat st b₄ <= b₅ holds
not b₂ . b₅ in b₃

proof end;

theorem Th7: :: FRECHET2:7

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁
for b₃, b₄ being Subset of b₁ st rng b₂ c= b₃ \/ b₄ holds
ex b₅ being subsequence of b₂ st
( rng b₅ c= b₃ or rng b₅ c= b₄ )

proof end;

Lemma17: for b₁ being non empty TopSpace st b₁ is first-countable holds
for b₂ being Point of b₁ ex b₃ being Basis of b₂ex b₄ being Function st
( dom b₄ = NAT & rng b₄ = b₃ & ( for b₅, b₆ being Nat st b₆ >= b₅ holds
b₄ . b₆ c= b₄ . b₅ ) )

proof end;

theorem Th8: :: FRECHET2:8

for b₁ being non empty TopSpace st ( for b₂ being sequence of b₁
for b₃, b₄ being Point of b₁ st b₃ in Lim b₂ & b₄ in Lim b₂ holds
b₃ = b₄ ) holds
b₁ is_T1

proof end;

theorem Th9: :: FRECHET2:9

for b₁ being non empty TopSpace st b₁ is_T2 holds
for b₂ being sequence of b₁
for b₃, b₄ being Point of b₁ st b₃ in Lim b₂ & b₄ in Lim b₂ holds
b₃ = b₄

proof end;

theorem Th10: :: FRECHET2:10

for b₁ being non empty TopSpace st b₁ is first-countable holds
( b₁ is_T2 iff for b₂ being sequence of b₁
for b₃, b₄ being Point of b₁ st b₃ in Lim b₂ & b₄ in Lim b₂ holds
b₃ = b₄ )

proof end;

theorem Th11: :: FRECHET2:11

for b₁ being non empty TopStruct
for b₂ being sequence of b₁ st not b₂ is convergent holds
Lim b₂ = {}

proof end;

theorem Th12: :: FRECHET2:12

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

proof end;

theorem Th13: :: FRECHET2:13

for b₁ being non empty TopStruct
for b₂ being sequence of b₁
for b₃ being Point of b₁ st not b₂ is_convergent_to b₃ holds
ex b₄ being subsequence of b₂ st
for b₅ being subsequence of b₄ holds not b₅ is_convergent_to b₃

proof end;

theorem Th14: :: FRECHET2:14

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ st b₃ is continuous holds
for b₄ being sequence of b₁
for b₅ being sequence of b₂ st b₅ = b₃ * b₄ holds
b₃ .: (Lim b₄) c= Lim b₅

proof end;

theorem Th15: :: FRECHET2:15

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ st b₁ is sequential holds
( b₃ is continuous iff for b₄ being sequence of b₁
for b₅ being sequence of b₂ st b₅ = b₃ * b₄ holds
b₃ .: (Lim b₄) c= Lim b₅ )

proof end;

definition

let c₁ be non empty TopStruct ;
let c₂ be Subset of c₁;
canceled;
func Cl_Seq c₂ -> Subset of a₁ means :Def2: :: FRECHET2:def 2
for b₁ being Point of a₁ holds
( b₁ in a₃ iff ex b₂ being sequence of a₁ st
( rng b₂ c= a₂ & b₁ in Lim b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 FRECHET2:def 1 :

:: deftheorem Def2 defines Cl_Seq FRECHET2:def 2 :

theorem Th16: :: FRECHET2:16

for b₁ being non empty TopStruct
for b₂ being Subset of b₁
for b₃ being sequence of b₁
for b₄ being Point of b₁ st rng b₃ c= b₂ & b₄ in Lim b₃ holds
b₄ in Cl b₂

proof end;

theorem Th17: :: FRECHET2:17

for b₁ being non empty TopStruct
for b₂ being Subset of b₁ holds Cl_Seq b₂ c= Cl b₂

proof end;

theorem Th18: :: FRECHET2:18

for b₁ being non empty TopStruct
for b₂ being sequence of b₁
for b₃ being subsequence of b₂
for b₄ being Point of b₁ st b₂ is_convergent_to b₄ holds
b₃ is_convergent_to b₄

proof end;

theorem Th19: :: FRECHET2:19

for b₁ being non empty TopStruct
for b₂ being sequence of b₁
for b₃ being subsequence of b₂ holds Lim b₂ c= Lim b₃

proof end;

theorem Th20: :: FRECHET2:20

for b₁ being non empty TopStruct holds Cl_Seq ({} b₁) = {}

proof end;

theorem Th21: :: FRECHET2:21

for b₁ being non empty TopStruct
for b₂ being Subset of b₁ holds b₂ c= Cl_Seq b₂

proof end;

theorem Th22: :: FRECHET2:22

for b₁ being non empty TopStruct
for b₂, b₃ being Subset of b₁ holds (Cl_Seq b₂) \/ (Cl_Seq b₃) = Cl_Seq (b₂ \/ b₃)

proof end;

theorem Th23: :: FRECHET2:23

for b₁ being non empty TopStruct holds
( b₁ is Frechet iff for b₂ being Subset of b₁ holds Cl b₂ = Cl_Seq b₂ )

proof end;

theorem Th24: :: FRECHET2:24

for b₁ being non empty TopSpace st b₁ is Frechet holds
for b₂, b₃ being Subset of b₁ holds
( Cl_Seq ({} b₁) = {} & b₂ c= Cl_Seq b₂ & Cl_Seq (b₂ \/ b₃) = (Cl_Seq b₂) \/ (Cl_Seq b₃) & Cl_Seq (Cl_Seq b₂) = Cl_Seq b₂ )

proof end;

theorem Th25: :: FRECHET2:25

for b₁ being non empty TopSpace st b₁ is sequential & ( for b₂ being Subset of b₁ holds Cl_Seq (Cl_Seq b₂) = Cl_Seq b₂ ) holds
b₁ is Frechet

proof end;

theorem Th26: :: FRECHET2:26

for b₁ being non empty TopSpace st b₁ is sequential holds
( b₁ is Frechet iff for b₂, b₃ being Subset of b₁ holds
( Cl_Seq ({} b₁) = {} & b₂ c= Cl_Seq b₂ & Cl_Seq (b₂ \/ b₃) = (Cl_Seq b₂) \/ (Cl_Seq b₃) & Cl_Seq (Cl_Seq b₂) = Cl_Seq b₂ ) ) by Th24, Th25;

definition

let c₁ be non empty TopSpace;
let c₂ be sequence of c₁;
assume E33: ex b₁ being Point of c₁ st Lim c₂ = {b₁} ;
func lim c₂ -> Point of a₁ means :Def3: :: FRECHET2:def 3
a₂ is_convergent_to a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines lim FRECHET2:def 3 :

theorem Th27: :: FRECHET2:27

for b₁ being non empty TopSpace st b₁ is_T2 holds
for b₂ being sequence of b₁ st b₂ is convergent holds
ex b₃ being Point of b₁ st Lim b₂ = {b₃}

proof end;

theorem Th28: :: FRECHET2:28

for b₁ being non empty TopSpace st b₁ is_T2 holds
for b₂ being sequence of b₁
for b₃ being Point of b₁ holds
( b₂ is_convergent_to b₃ iff ( b₂ is convergent & b₃ = lim b₂ ) )

proof end;

theorem Th29: :: FRECHET2:29

for b₁ being MetrStruct
for b₂ being sequence of b₁ holds b₂ is sequence of (TopSpaceMetr b₁)

proof end;

theorem Th30: :: FRECHET2:30

for b₁ being non empty MetrStruct
for b₂ being sequence of (TopSpaceMetr b₁) holds b₂ is sequence of b₁

proof end;

theorem Th31: :: FRECHET2:31

for b₁ being non empty MetrSpace
for b₂ being sequence of b₁
for b₃ being Point of b₁
for b₄ being sequence of (TopSpaceMetr b₁)
for b₅ being Point of (TopSpaceMetr b₁) st b₂ = b₄ & b₃ = b₅ holds
( b₂ is_convergent_in_metrspace_to b₃ iff b₄ is_convergent_to b₅ )

proof end;

theorem Th32: :: FRECHET2:32

for b₁ being non empty MetrSpace
for b₂ being sequence of b₁
for b₃ being sequence of (TopSpaceMetr b₁) st b₂ = b₃ holds
( b₂ is convergent iff b₃ is convergent )

proof end;

theorem Th33: :: FRECHET2:33

for b₁ being non empty MetrSpace
for b₂ being sequence of b₁
for b₃ being sequence of (TopSpaceMetr b₁) st b₂ = b₃ & b₂ is convergent holds
lim b₂ = lim b₃

proof end;

definition

let c₁ be TopStruct ;
let c₂ be sequence of c₁;
let c₃ be Point of c₁;
pred c₃ is_a_cluster_point_of c₂ means :Def4: :: FRECHET2:def 4
for b₁ being Subset of a₁
for b₂ being Nat st b₁ is open & a₃ in b₁ holds
ex b₃ being Nat st
( b₂ <= b₃ & a₂ . b₃ in b₁ );

end;

:: deftheorem Def4 defines is_a_cluster_point_of FRECHET2:def 4 :

theorem Th34: :: FRECHET2:34

for b₁ being non empty TopStruct
for b₂ being sequence of b₁
for b₃ being Point of b₁ st ex b₄ being subsequence of b₂ st b₄ is_convergent_to b₃ holds
b₃ is_a_cluster_point_of b₂

proof end;

theorem Th35: :: FRECHET2:35

for b₁ being non empty TopStruct
for b₂ being sequence of b₁
for b₃ being Point of b₁ st b₂ is_convergent_to b₃ holds
b₃ is_a_cluster_point_of b₂

proof end;

theorem Th36: :: FRECHET2:36

for b₁ being non empty TopStruct
for b₂ being sequence of b₁
for b₃ being Point of b₁
for b₄ being Subset of b₁ st b₄ = { b₅ where B is Point of b₁ : b₃ in Cl {b₅} } & rng b₂ c= b₄ holds
b₂ is_convergent_to b₃

proof end;

theorem Th37: :: FRECHET2:37

for b₁ being non empty TopStruct
for b₂ being sequence of b₁
for b₃, b₄ being Point of b₁ st ( for b₅ being Nat holds
( b₂ . b₅ = b₄ & b₂ is_convergent_to b₃ ) ) holds
b₃ in Cl {b₄}

proof end;

theorem Th38: :: FRECHET2:38

for b₁ being non empty TopStruct
for b₂ being Point of b₁
for b₃ being Subset of b₁
for b₄ being sequence of b₁ st b₃ = { b₅ where B is Point of b₁ : b₂ in Cl {b₅} } & rng b₄ misses b₃ & b₄ is_convergent_to b₂ holds
ex b₅ being subsequence of b₄ st b₅ is one-to-one

proof end;

Lemma42: for b₁ being Function st not dom b₁ is finite & b₁ is one-to-one holds
not rng b₁ is finite

proof end;

theorem Th39: :: FRECHET2:39

for b₁ being non empty TopStruct
for b₂, b₃ being sequence of b₁ st rng b₃ c= rng b₂ & b₃ is one-to-one holds
ex b₄ being Permutation of NAT st b₃ * b₄ is subsequence of b₂

proof end;

scheme :: FRECHET2:sch 3
s3{ F₁() -> non empty 1-sorted , F₂() -> sequence of F₁(), F₃() -> Permutation of NAT , P₁[ set ] } :

ex b₁ being Nat st
for b₂ being Nat st b₁ <= b₂ holds
P₁[(F₂() * F₃()) . b₂]

provided

E44: ex b₁ being Nat st
for b₂ being Nat
for b₃ being Point of F₁() st b₁ <= b₂ & b₃ = F₂() . b₂ holds
P₁[b₃]

proof end;

scheme :: FRECHET2:sch 4
s4{ F₁() -> non empty TopStruct , F₂() -> sequence of F₁(), F₃() -> Permutation of NAT , P₁[ set ] } :

ex b₁ being Nat st
for b₂ being Nat st b₁ <= b₂ holds
P₁[(F₂() * F₃()) . b₂]

provided

E44: ex b₁ being Nat st
for b₂ being Nat
for b₃ being Point of F₁() st b₁ <= b₂ & b₃ = F₂() . b₂ holds
P₁[b₃]

proof end;

theorem Th40: :: FRECHET2:40

for b₁ being non empty TopStruct
for b₂ being sequence of b₁
for b₃ being Permutation of NAT
for b₄ being Point of b₁ st b₂ is_convergent_to b₄ holds
b₂ * b₃ is_convergent_to b₄

proof end;

theorem Th41: :: FRECHET2:41

for b₁ being Nat ex b₂ being increasing Seq_of_Nat st
for b₃ being Nat holds b₂ . b₃ = b₃ + b₁

proof end;

theorem Th42: :: FRECHET2:42

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁
for b₃ being Nat ex b₄ being subsequence of b₂ st
for b₅ being Nat holds b₄ . b₅ = b₂ . (b₅ + b₃)

proof end;

theorem Th43: :: FRECHET2:43

for b₁ being non empty TopStruct
for b₂ being sequence of b₁
for b₃ being Point of b₁
for b₄ being subsequence of b₂ st b₃ is_a_cluster_point_of b₂ & ex b₅ being Nat st
for b₆ being Nat holds b₄ . b₆ = b₂ . (b₆ + b₅) holds
b₃ is_a_cluster_point_of b₄

proof end;

theorem Th44: :: FRECHET2:44

for b₁ being non empty TopStruct
for b₂ being sequence of b₁
for b₃ being Point of b₁ st b₃ is_a_cluster_point_of b₂ holds
b₃ in Cl (rng b₂)

proof end;

theorem Th45: :: FRECHET2:45

for b₁ being non empty TopStruct st b₁ is Frechet holds
for b₂ being sequence of b₁
for b₃ being Point of b₁ st b₃ is_a_cluster_point_of b₂ holds
ex b₄ being subsequence of b₂ st b₄ is_convergent_to b₃

proof end;

theorem Th46: :: FRECHET2:46

for b₁ being non empty TopSpace st b₁ is first-countable holds
for b₂ being Point of b₁ ex b₃ being Basis of b₂ex b₄ being Function st
( dom b₄ = NAT & rng b₄ = b₃ & ( for b₅, b₆ being Nat st b₆ >= b₅ holds
b₄ . b₆ c= b₄ . b₅ ) ) by Lemma17;

theorem Th47: :: FRECHET2:47

for b₁ being non empty TopSpace holds
( b₁ is_T1 iff for b₂ being Point of b₁ holds Cl {b₂} = {b₂} ) by Lemma1;

theorem Th48: :: FRECHET2:48

for b₁ being non empty TopSpace st b₁ is_T2 holds
b₁ is_T1 by Lemma4;

theorem Th49: :: FRECHET2:49

for b₁ being non empty TopSpace st not b₁ is_T1 holds
ex b₂, b₃ being Point of b₁ex b₄ being sequence of b₁ st
( b₄ = NAT --> b₂ & b₂ <> b₃ & b₄ is_convergent_to b₃ ) by Lemma3;

theorem Th50: :: FRECHET2:50

for b₁ being Function st not dom b₁ is finite & b₁ is one-to-one holds
not rng b₁ is finite by Lemma42;