:: by Bart{\l}omiej Skorulski

::

:: Received February 13, 1999

:: Copyright (c) 1999-2017 Association of Mizar Users

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

T is T_1

proof end;

Lm2: for T being non empty TopSpace st not T is T_1 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 T_1 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 T_2 holds

T is T_1

proof end;

theorem :: FRECHET2:1

theorem :: FRECHET2:2

theorem Th3: :: FRECHET2:3

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 Element of NAT st

for m being Element of NAT st n <= m holds

not S . m in A

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 Element of NAT st

for m being Element of NAT st n <= m holds

not S . m in A

proof end;

theorem Th4: :: FRECHET2:4

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 )

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;

Lm5: 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 Element of NAT st m >= n holds

S . m c= S . n ) )

proof end;

theorem :: FRECHET2:5

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 T_1

for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds

x1 = x2 ) holds

T is T_1

proof end;

theorem Th6: :: FRECHET2:6

for T being non empty TopSpace st T is T_2 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

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

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

( T is T_2 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 )

( T is T_2 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 :: FRECHET2:10

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

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 Th11: :: FRECHET2:11

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

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

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 )

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;

ex b_{1} being Subset of T st

for x being Point of T holds

( x in b_{1} iff ex S being sequence of T st

( rng S c= A & x in Lim S ) )

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

( x in b_{1} iff ex S being sequence of T st

( rng S c= A & x in Lim S ) ) ) & ( for x being Point of T holds

( x in b_{2} iff ex S being sequence of T st

( rng S c= A & x in Lim S ) ) ) holds

b_{1} = b_{2}

end;
let A be Subset of T;

func Cl_Seq A -> Subset of T means :Def1: :: FRECHET2:def 1

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

ex b

for x being Point of T holds

( x in b

( rng S c= A & x in Lim S ) )

proof end;

uniqueness for b

( x in b

( rng S c= A & x in Lim S ) ) ) & ( for x being Point of T holds

( x in b

( rng S c= A & x in Lim S ) ) ) holds

b

proof end;

:: deftheorem Def1 defines Cl_Seq FRECHET2:def 1 :

for T being non empty TopStruct

for A, b_{3} being Subset of T holds

( b_{3} = Cl_Seq A iff for x being Point of T holds

( x in b_{3} iff ex S being sequence of T st

( rng S c= A & x in Lim S ) ) );

for T being non empty TopStruct

for A, b

( b

( x in b

( rng S c= A & x in Lim S ) ) );

theorem Th13: :: FRECHET2:13

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

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 Th15: :: FRECHET2:15

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

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 Th16: :: FRECHET2:16

for T being non empty TopStruct

for S being sequence of T

for S1 being subsequence of S holds Lim S c= Lim S1

for S being sequence of T

for S1 being subsequence of S holds Lim S c= Lim S1

proof end;

theorem Th19: :: FRECHET2:19

for T being non empty TopStruct

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

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

proof end;

theorem Th20: :: FRECHET2:20

for T being non empty TopStruct holds

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

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

proof end;

theorem Th21: :: FRECHET2:21

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 )

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 Th22: :: FRECHET2:22

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

T is Frechet

proof end;

theorem :: FRECHET2:23

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

existence

ex b_{1} being Point of T st S is_convergent_to b_{1}

for b_{1}, b_{2} being Point of T st S is_convergent_to b_{1} & S is_convergent_to b_{2} holds

b_{1} = b_{2}

end;
let S be sequence of T;

assume A1: ex x being Point of T st Lim S = {x} ;

existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines lim FRECHET2:def 2 :

for T being non empty TopSpace

for S being sequence of T st ex x being Point of T st Lim S = {x} holds

for b_{3} being Point of T holds

( b_{3} = lim S iff S is_convergent_to b_{3} );

for T being non empty TopSpace

for S being sequence of T st ex x being Point of T st Lim S = {x} holds

for b

( b

theorem Th24: :: FRECHET2:24

for T being non empty TopSpace st T is T_2 holds

for S being sequence of T st S is convergent holds

ex x being Point of T st Lim S = {x}

for S being sequence of T st S is convergent holds

ex x being Point of T st Lim S = {x}

proof end;

theorem Th25: :: FRECHET2:25

for T being non empty TopSpace st T is T_2 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 ) )

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

for M being non empty MetrStruct

for S being sequence of (TopSpaceMetr M) holds S is sequence of M by TOPMETR:12;

for S being sequence of (TopSpaceMetr M) holds S is sequence of M by TOPMETR:12;

theorem Th28: :: FRECHET2:28

for M being non empty MetrSpace

for S being sequence of M

for x being Point of M

for S9 being sequence of (TopSpaceMetr M)

for x9 being Point of (TopSpaceMetr M) st S = S9 & x = x9 holds

( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 )

for S being sequence of M

for x being Point of M

for S9 being sequence of (TopSpaceMetr M)

for x9 being Point of (TopSpaceMetr M) st S = S9 & x = x9 holds

( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 )

proof end;

theorem :: FRECHET2:29

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 )

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

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

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;

:: deftheorem defines is_a_cluster_point_of FRECHET2:def 3 :

for T being TopStruct

for S being sequence of T

for x being Point of T holds

( x is_a_cluster_point_of S iff for O being Subset of T

for n being Nat st O is open & x in O holds

ex m being Element of NAT st

( n <= m & S . m in O ) );

for T being TopStruct

for S being sequence of T

for x being Point of T holds

( x is_a_cluster_point_of S iff for O being Subset of T

for n being Nat st O is open & x in O holds

ex m being Element of NAT st

( n <= m & S . m in O ) );

theorem Th31: :: FRECHET2:31

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

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

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

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

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

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

for T being non empty TopStruct

for S being sequence of T

for x, y being Point of T st ( for n being Element of NAT holds

( S . n = y & S is_convergent_to x ) ) holds

x in Cl {y}

for S being sequence of T

for x, y being Point of T st ( for n being Element of NAT holds

( S . n = y & S is_convergent_to x ) ) holds

x in Cl {y}

proof end;

theorem Th35: :: FRECHET2:35

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

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;

theorem Th36: :: FRECHET2:36

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

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 1

PermSeq{ F_{1}() -> non empty 1-sorted , F_{2}() -> sequence of F_{1}(), F_{3}() -> Permutation of NAT, P_{1}[ set ] } :

PermSeq{ F

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

P_{1}[(F_{2}() * F_{3}()) . m]

providedfor m being Element of NAT st n <= m holds

P

A1:
ex n being Element of NAT st

for m being Element of NAT

for x being Point of F_{1}() st n <= m & x = F_{2}() . m holds

P_{1}[x]

for m being Element of NAT

for x being Point of F

P

proof end;

scheme :: FRECHET2:sch 2

PermSeq2{ F_{1}() -> non empty TopStruct , F_{2}() -> sequence of F_{1}(), F_{3}() -> Permutation of NAT, P_{1}[ set ] } :

PermSeq2{ F

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

P_{1}[(F_{2}() * F_{3}()) . m]

providedfor m being Element of NAT st n <= m holds

P

A1:
ex n being Element of NAT st

for m being Element of NAT

for x being Point of F_{1}() st n <= m & x = F_{2}() . m holds

P_{1}[x]

for m being Element of NAT

for x being Point of F

P

proof end;

theorem Th37: :: FRECHET2:37

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

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

for n0 being Element of NAT ex NS being increasing sequence of NAT st

for n being Element of NAT holds NS . n = n + n0

for n being Element of NAT holds NS . n = n + n0

proof end;

theorem Th39: :: FRECHET2:39

for T being non empty TopStruct

for S being sequence of T

for x being Point of T

for n0 being Nat st x is_a_cluster_point_of S holds

x is_a_cluster_point_of S ^\ n0

for S being sequence of T

for x being Point of T

for n0 being Nat st x is_a_cluster_point_of S holds

x is_a_cluster_point_of S ^\ n0

proof end;

theorem Th40: :: FRECHET2:40

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)

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

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

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

theorem :: FRECHET2:43

theorem :: FRECHET2:45