:: FRECHET2 semantic presentation

Lm1: for T being non empty TopSpace holds
( T is_T1 iff for p being Point of T holds Cl {p} = {p} )

proof end;

Lm2: for T being non empty TopSpace st not T is_T1 holds
ex x1, x2 being Point of T st
( x1 <> x2 & x2 in Cl {x1} )

proof end;

Lm3: for T being non empty TopSpace st not T is_T1 holds
ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 )

proof end;

Lm4: for T being non empty TopSpace st T is_T2 holds
T is_T1

proof end;

Lm5: for T being non empty 1-sorted
for S being sequence of T
for f being Function of NAT , NAT holds S * f is sequence of T
;

definition

let T be non empty 1-sorted ;
let f be Function of NAT , NAT ;
let S be sequence of T;
:: original: *
redefine func S * f -> sequence of T;
coherence by Lm5;

end;

theorem Th1: :: FRECHET2:1

for T being non empty 1-sorted
for S being sequence of T
for NS being increasing Seq_of_Nat holds S * NS is sequence of T

proof end;

Lm6: id NAT is Real_Sequence

proof end;

Lm7: for RS being Real_Sequence st RS = id NAT holds
RS is natural-yielding

proof end;

Lm8: for RS being Real_Sequence st RS = id NAT holds
RS is increasing

proof end;

theorem :: FRECHET2:2

for RS being Real_Sequence st RS = id NAT holds
RS is increasing Seq_of_Nat by Lm7, Lm8;

Lm9: for T being non empty 1-sorted
for S being sequence of T ex NS being increasing Seq_of_Nat st S = S * NS

proof end;

theorem Th3: :: FRECHET2:3

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

proof end;

theorem Th4: :: FRECHET2:4

for T being non empty 1-sorted
for S being sequence of T
for S1 being subsequence of S holds rng S1 c= rng S

proof end;

Lm10: for T being non empty 1-sorted
for S being sequence of T
for NS being increasing Seq_of_Nat holds S * NS is subsequence of S

proof end;

definition

let T be non empty 1-sorted ;
let NS be increasing Seq_of_Nat;
let S be sequence of T;
:: original: *
redefine func S * NS -> subsequence of S;
correctness by Lm10;

end;

theorem Th5: :: FRECHET2:5

for T being non empty 1-sorted
for S1 being sequence of T
for S2 being subsequence of S1
for S3 being subsequence of S2 holds S3 is subsequence of S1

proof end;

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

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

provided

A1: for n being Nat ex m being Nat ex x being Point of F₁() st
( n <= m & x = F₂() . m & P₁[x] )

proof end;

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

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

provided

A1: for n being Nat ex m being Nat ex x being Point of F₁() st
( n <= m & x = F₂() . m & P₁[x] )

proof end;

theorem Th6: :: FRECHET2:6

for T being non empty 1-sorted
for S being sequence of T
for A being Subset of T st ( for S1 being subsequence of S holds not rng S1 c= A ) holds
ex n being Nat st
for m being Nat st n <= m holds
not S . m in A

proof end;

theorem Th7: :: FRECHET2:7

for T being non empty 1-sorted
for S being sequence of T
for A, B being Subset of T st rng S c= A \/ B holds
ex S1 being subsequence of S st
( rng S1 c= A or rng S1 c= B )

proof end;

Lm11: for T being non empty TopSpace st T is first-countable holds
for x being Point of T ex B being Basis of x ex S being Function st
( dom S = NAT & rng S = B & ( for n, m being Nat st m >= n holds
S . m c= S . n ) )

proof end;

theorem :: FRECHET2:8

for T being non empty TopSpace st ( for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 ) holds
T is_T1

proof end;

theorem Th9: :: FRECHET2:9

for T being non empty TopSpace st T is_T2 holds
for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2

proof end;

theorem :: FRECHET2:10

for T being non empty TopSpace st T is first-countable holds
( T is_T2 iff for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 )

proof end;

theorem Th11: :: FRECHET2:11

for T being non empty TopStruct
for S being sequence of T st not S is convergent holds
Lim S = {}

proof end;

theorem Th12: :: FRECHET2:12

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 :: FRECHET2:13

for T being non empty TopStruct
for S being sequence of T
for x being Point of T st not S is_convergent_to x holds
ex S1 being subsequence of S st
for S2 being subsequence of S1 holds not S2 is_convergent_to x

proof end;

theorem Th14: :: FRECHET2:14

for T1, T2 being non empty TopSpace
for f being Function of T1,T2 st f is continuous holds
for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2

proof end;

theorem :: FRECHET2:15

for T1, T2 being non empty TopSpace
for f being Function of T1,T2 st T1 is sequential holds
( f is continuous iff for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 )

proof end;

definition

let T be non empty TopStruct ;
let A be Subset of T;
canceled;
func Cl_Seq A -> Subset of T means :Def2: :: FRECHET2:def 2
for x being Point of T holds
( x in it iff ex S being sequence of T st
( rng S c= A & x in Lim S ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem FRECHET2:def 1 :

:: deftheorem Def2 defines Cl_Seq FRECHET2:def 2 :

theorem Th16: :: FRECHET2:16

for T being non empty TopStruct
for A being Subset of T
for S being sequence of T
for x being Point of T st rng S c= A & x in Lim S holds
x in Cl A

proof end;

theorem Th17: :: FRECHET2:17

for T being non empty TopStruct
for A being Subset of T holds Cl_Seq A c= Cl A

proof end;

theorem Th18: :: FRECHET2:18

for T being non empty TopStruct
for S being sequence of T
for S1 being subsequence of S
for x being Point of T st S is_convergent_to x holds
S1 is_convergent_to x

proof end;

theorem Th19: :: FRECHET2:19

for T being non empty TopStruct
for S being sequence of T
for S1 being subsequence of S holds Lim S c= Lim S1

proof end;

theorem Th20: :: FRECHET2:20

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

proof end;

theorem Th21: :: FRECHET2:21

for T being non empty TopStruct
for A being Subset of T holds A c= Cl_Seq A

proof end;

theorem Th22: :: FRECHET2:22

for T being non empty TopStruct
for A, B being Subset of T holds (Cl_Seq A) \/ (Cl_Seq B) = Cl_Seq (A \/ B)

proof end;

theorem Th23: :: FRECHET2:23

for T being non empty TopStruct holds
( T is Frechet iff for A being Subset of T holds Cl A = Cl_Seq A )

proof end;

theorem Th24: :: FRECHET2:24

for T being non empty TopSpace st T is Frechet holds
for A, B being Subset of T holds
( Cl_Seq ({} T) = {} & A c= Cl_Seq A & Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) & Cl_Seq (Cl_Seq A) = Cl_Seq A )

proof end;

theorem Th25: :: FRECHET2:25

for T being non empty TopSpace st T is sequential & ( for A being Subset of T holds Cl_Seq (Cl_Seq A) = Cl_Seq A ) holds
T is Frechet

proof end;

theorem :: FRECHET2:26

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

definition

let T be non empty TopSpace;
let S be sequence of T;
assume A1: ex x being Point of T st Lim S = {x} ;
func lim S -> Point of T means :Def3: :: FRECHET2:def 3
S is_convergent_to it;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines lim FRECHET2:def 3 :

theorem Th27: :: FRECHET2:27

for T being non empty TopSpace st T is_T2 holds
for S being sequence of T st S is convergent holds
ex x being Point of T st Lim S = {x}

proof end;

theorem Th28: :: FRECHET2:28

for T being non empty TopSpace st T is_T2 holds
for S being sequence of T
for x being Point of T holds
( S is_convergent_to x iff ( S is convergent & x = lim S ) )

proof end;

theorem :: FRECHET2:29

for M being MetrStruct
for S being sequence of M holds S is sequence of (TopSpaceMetr M)

proof end;

theorem :: FRECHET2:30

for M being non empty MetrStruct
for S being sequence of (TopSpaceMetr M) holds S is sequence of M

proof end;

theorem Th31: :: FRECHET2:31

for M being non empty MetrSpace
for S being sequence of M
for x being Point of M
for S' being sequence of (TopSpaceMetr M)
for x' being Point of (TopSpaceMetr M) st S = S' & x = x' holds
( S is_convergent_in_metrspace_to x iff S' is_convergent_to x' )

proof end;

theorem :: FRECHET2:32

for M being non empty MetrSpace
for Sm being sequence of M
for St being sequence of (TopSpaceMetr M) st Sm = St holds
( Sm is convergent iff St is convergent )

proof end;

theorem :: FRECHET2:33

for M being non empty MetrSpace
for Sm being sequence of M
for St being sequence of (TopSpaceMetr M) st Sm = St & Sm is convergent holds
lim Sm = lim St

proof end;

definition

let T be TopStruct ;
let S be sequence of T;
let x be Point of T;
pred x is_a_cluster_point_of S means :Def4: :: FRECHET2:def 4
for O being Subset of T
for n being Nat st O is open & x in O holds
ex m being Nat st
( n <= m & S . m in O );

end;

:: deftheorem Def4 defines is_a_cluster_point_of FRECHET2:def 4 :

theorem Th34: :: FRECHET2:34

for T being non empty TopStruct
for S being sequence of T
for x being Point of T st ex S1 being subsequence of S st S1 is_convergent_to x holds
x is_a_cluster_point_of S

proof end;

theorem :: FRECHET2:35

for T being non empty TopStruct
for S being sequence of T
for x being Point of T st S is_convergent_to x holds
x is_a_cluster_point_of S

proof end;

theorem Th36: :: FRECHET2:36

for T being non empty TopStruct
for S being sequence of T
for x being Point of T
for Y being Subset of T st Y = { y where y is Point of T : x in Cl {y} } & rng S c= Y holds
S is_convergent_to x

proof end;

theorem Th37: :: FRECHET2:37

for T being non empty TopStruct
for S being sequence of T
for x, y being Point of T st ( for n being Nat holds
( S . n = y & S is_convergent_to x ) ) holds
x in Cl {y}

proof end;

theorem Th38: :: FRECHET2:38

for T being non empty TopStruct
for x being Point of T
for Y being Subset of T
for S being sequence of T st Y = { y where y is Point of T : x in Cl {y} } & rng S misses Y & S is_convergent_to x holds
ex S1 being subsequence of S st S1 is one-to-one

proof end;

Lm12: for f being Function st not dom f is finite & f is one-to-one holds
not rng f is finite

proof end;

theorem Th39: :: FRECHET2:39

for T being non empty TopStruct
for S1, S2 being sequence of T st rng S2 c= rng S1 & S2 is one-to-one holds
ex P being Permutation of NAT st S2 * P is subsequence of S1

proof end;

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

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

provided

A1: ex n being Nat st
for m being Nat
for x being Point of F₁() st n <= m & x = F₂() . m holds
P₁[x]

proof end;

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

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

provided

A1: ex n being Nat st
for m being Nat
for x being Point of F₁() st n <= m & x = F₂() . m holds
P₁[x]

proof end;

theorem Th40: :: FRECHET2:40

for T being non empty TopStruct
for S being sequence of T
for P being Permutation of NAT
for x being Point of T st S is_convergent_to x holds
S * P is_convergent_to x

proof end;

theorem Th41: :: FRECHET2:41

for n0 being Nat ex NS being increasing Seq_of_Nat st
for n being Nat holds NS . n = n + n0

proof end;

theorem Th42: :: FRECHET2:42

for T being non empty 1-sorted
for S being sequence of T
for n0 being Nat ex S1 being subsequence of S st
for n being Nat holds S1 . n = S . (n + n0)

proof end;

theorem Th43: :: FRECHET2:43

for T being non empty TopStruct
for S being sequence of T
for x being Point of T
for S1 being subsequence of S st x is_a_cluster_point_of S & ex n0 being Nat st
for n being Nat holds S1 . n = S . (n + n0) holds
x is_a_cluster_point_of S1

proof end;

theorem Th44: :: FRECHET2:44

for T being non empty TopStruct
for S being sequence of T
for x being Point of T st x is_a_cluster_point_of S holds
x in Cl (rng S)

proof end;

theorem :: FRECHET2:45

for T being non empty TopStruct st T is Frechet holds
for S being sequence of T
for x being Point of T st x is_a_cluster_point_of S holds
ex S1 being subsequence of S st S1 is_convergent_to x

proof end;

theorem :: FRECHET2:46

for T being non empty TopSpace st T is first-countable holds
for x being Point of T ex B being Basis of x ex S being Function st
( dom S = NAT & rng S = B & ( for n, m being Nat st m >= n holds
S . m c= S . n ) ) by Lm11;

theorem :: FRECHET2:47

for T being non empty TopSpace holds
( T is_T1 iff for p being Point of T holds Cl {p} = {p} ) by Lm1;

theorem :: FRECHET2:48

for T being non empty TopSpace st T is_T2 holds
T is_T1 by Lm4;

theorem :: FRECHET2:49

for T being non empty TopSpace st not T is_T1 holds
ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 ) by Lm3;

theorem :: FRECHET2:50

for f being Function st not dom f is finite & f is one-to-one holds
not rng f is finite by Lm12;