:: by Kazuhisa Nakasho , Keiko Narita and Yasunari Shidama

::

:: Received June 30, 2016

:: Copyright (c) 2016-2018 Association of Mizar Users

theorem LM1: :: TOPMETR4:1

for M being non empty set

for x being sequence of M st rng x is finite holds

ex z being Element of M st

( x " {z} c= NAT & x " {z} is infinite )

for x being sequence of M st rng x is finite holds

ex z being Element of M st

( x " {z} c= NAT & x " {z} is infinite )

proof end;

theorem LM2: :: TOPMETR4:2

for X being Subset of NAT st X is infinite holds

ex N being increasing sequence of NAT st rng N c= X

ex N being increasing sequence of NAT st rng N c= X

proof end;

theorem :: TOPMETR4:3

for M being non empty MetrSpace

for V being Subset of (TopSpaceMetr M) st V is open holds

ex F being Subset-Family of M st

( F = { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } & V = union F )

for V being Subset of (TopSpaceMetr M) st V is open holds

ex F being Subset-Family of M st

( F = { (Ball (x,r)) where x is Element of M, r is Real : ( r > 0 & Ball (x,r) c= V ) } & V = union F )

proof end;

theorem :: TOPMETR4:4

for M being non empty MetrSpace

for X being Subset of (TopSpaceMetr M)

for p being Element of M holds

( p in Cl X iff for r being Real st 0 < r holds

X meets Ball (p,r) )

for X being Subset of (TopSpaceMetr M)

for p being Element of M holds

( p in Cl X iff for r being Real st 0 < r holds

X meets Ball (p,r) )

proof end;

theorem Th3: :: TOPMETR4:5

for M being non empty MetrSpace

for X being Subset of (TopSpaceMetr M)

for x being object holds

( x in Cl X iff ex S being sequence of M st

( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x ) )

for X being Subset of (TopSpaceMetr M)

for x being object holds

( x in Cl X iff ex S being sequence of M st

( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x ) )

proof end;

theorem Th4: :: TOPMETR4:6

for M being non empty MetrSpace

for X being Subset of (TopSpaceMetr M) holds

( X is closed iff for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds

lim S in X )

for X being Subset of (TopSpaceMetr M) holds

( X is closed iff for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds

lim S in X )

proof end;

theorem :: TOPMETR4:7

for X, Y being non empty MetrSpace

for f being Function of (TopSpaceMetr X),(TopSpaceMetr Y) holds

( f is continuous iff for S being sequence of X

for T being sequence of Y st S is convergent & T = f * S holds

( T is convergent & lim T = f . (lim S) ) )

for f being Function of (TopSpaceMetr X),(TopSpaceMetr Y) holds

( f is continuous iff for S being sequence of X

for T being sequence of Y st S is convergent & T = f * S holds

( T is convergent & lim T = f . (lim S) ) )

proof end;

definition

let M be non empty MetrSpace;

let X be Subset of M;

end;
let X be Subset of M;

attr X is sequentially_compact means :Def1: :: TOPMETR4:def 1

for S1 being sequence of M st rng S1 c= X holds

ex S2 being sequence of M st

( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in X );

for S1 being sequence of M st rng S1 c= X holds

ex S2 being sequence of M st

( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in X );

:: deftheorem Def1 defines sequentially_compact TOPMETR4:def 1 :

for M being non empty MetrSpace

for X being Subset of M holds

( X is sequentially_compact iff for S1 being sequence of M st rng S1 c= X holds

ex S2 being sequence of M st

( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in X ) );

for M being non empty MetrSpace

for X being Subset of M holds

( X is sequentially_compact iff for S1 being sequence of M st rng S1 c= X holds

ex S2 being sequence of M st

( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in X ) );

Th6: for M being non empty MetrSpace

for X being Subset of M st X = {} holds

X is sequentially_compact

proof end;

registration

let M be non empty MetrSpace;

coherence

for b_{1} being Subset of M st b_{1} is empty holds

b_{1} is sequentially_compact
by Th6;

end;
coherence

for b

b

:: deftheorem defines sequentially_compact TOPMETR4:def 2 :

for M being non empty MetrSpace holds

( M is sequentially_compact iff [#] M is sequentially_compact );

for M being non empty MetrSpace holds

( M is sequentially_compact iff [#] M is sequentially_compact );

theorem Th7: :: TOPMETR4:8

for M being non empty MetrSpace

for X being Subset of M

for Y being Subset of (TopSpaceMetr M)

for x being Element of M

for y being Element of (TopSpaceMetr M) st X = Y & x = y holds

( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds

Ball (x,r) meets X \ {x} )

for X being Subset of M

for Y being Subset of (TopSpaceMetr M)

for x being Element of M

for y being Element of (TopSpaceMetr M) st X = Y & x = y holds

( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds

Ball (x,r) meets X \ {x} )

proof end;

LM3: for M being non empty MetrSpace

for X being Subset of M

for x being Element of M st ( for r being Real st 0 < r holds

Ball (x,r) meets X \ {x} ) holds

for r being Real st 0 < r holds

(Ball (x,r)) /\ (X \ {x}) is infinite

proof end;

theorem Th8: :: TOPMETR4:9

for M being non empty MetrSpace st TopSpaceMetr M is countably_compact holds

M is sequentially_compact

M is sequentially_compact

proof end;

theorem :: TOPMETR4:10

for M being non empty MetrSpace st M is sequentially_compact holds

TopSpaceMetr M is countably_compact

TopSpaceMetr M is countably_compact

proof end;

Th10: for M being non empty MetrSpace st M is sequentially_compact holds

( M is totally_bounded & M is complete )

proof end;

theorem Th12: :: TOPMETR4:12

for M being non empty MetrSpace holds

( ( M is totally_bounded & M is complete ) iff M is sequentially_compact )

( ( M is totally_bounded & M is complete ) iff M is sequentially_compact )

proof end;

theorem Th14: :: TOPMETR4:13

for M being non empty MetrSpace

for S being non empty Subset of M holds

( S is sequentially_compact iff M | S is sequentially_compact )

for S being non empty Subset of M holds

( S is sequentially_compact iff M | S is sequentially_compact )

proof end;

theorem :: TOPMETR4:14

for M being non empty MetrSpace

for S being non empty Subset of M holds

( S is sequentially_compact iff M | S is compact )

for S being non empty Subset of M holds

( S is sequentially_compact iff M | S is compact )

proof end;

theorem Th16: :: TOPMETR4:15

for M being non empty MetrSpace

for S being Subset of M

for T being Subset of (TopSpaceMetr M) st T = S holds

( T is compact iff S is sequentially_compact )

for S being Subset of M

for T being Subset of (TopSpaceMetr M) st T = S holds

( T is compact iff S is sequentially_compact )

proof end;

theorem :: TOPMETR4:16

for M being non empty MetrSpace

for S being non empty Subset of M

for T being non empty Subset of (TopSpaceMetr M) st T = S holds

( (TopSpaceMetr M) | T is countably_compact iff S is sequentially_compact )

for S being non empty Subset of M

for T being non empty Subset of (TopSpaceMetr M) st T = S holds

( (TopSpaceMetr M) | T is countably_compact iff S is sequentially_compact )

proof end;

theorem :: TOPMETR4:17

for M being non empty MetrSpace

for S being non empty Subset of M holds

( ( M | S is totally_bounded & M | S is complete ) iff S is sequentially_compact )

for S being non empty Subset of M holds

( ( M | S is totally_bounded & M | S is complete ) iff S is sequentially_compact )

proof end;

theorem Th19: :: TOPMETR4:18

for NrSp being RealNormSpace

for S being Subset of NrSp

for T being Subset of (MetricSpaceNorm NrSp) st S = T holds

( S is compact iff T is sequentially_compact )

for S being Subset of NrSp

for T being Subset of (MetricSpaceNorm NrSp) st S = T holds

( S is compact iff T is sequentially_compact )

proof end;

theorem :: TOPMETR4:19

for NrSp being RealNormSpace

for S being Subset of NrSp

for T being Subset of (TopSpaceNorm NrSp) st S = T holds

( S is compact iff T is compact )

for S being Subset of NrSp

for T being Subset of (TopSpaceNorm NrSp) st S = T holds

( S is compact iff T is compact )

proof end;

theorem Th23: :: TOPMETR4:20

for S1 being sequence of RealSpace

for seq being Real_Sequence

for g being Real

for g1 being Element of RealSpace st S1 = seq & g = g1 holds

( ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - g).| < p ) iff for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

dist ((S1 . m),g1) < p )

for seq being Real_Sequence

for g being Real

for g1 being Element of RealSpace st S1 = seq & g = g1 holds

( ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - g).| < p ) iff for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

dist ((S1 . m),g1) < p )

proof end;

theorem :: TOPMETR4:21

for S1 being sequence of RealSpace

for seq being Real_Sequence

for g being Real

for g1 being Element of RealSpace st S1 = seq & g = g1 holds

( seq is convergent & lim seq = g iff ( S1 is convergent & lim S1 = g1 ) )

for seq being Real_Sequence

for g being Real

for g1 being Element of RealSpace st S1 = seq & g = g1 holds

( seq is convergent & lim seq = g iff ( S1 is convergent & lim S1 = g1 ) )

proof end;

theorem :: TOPMETR4:22

for S1 being sequence of RealSpace

for seq being Real_Sequence st S1 = seq & seq is convergent holds

( S1 is convergent & lim S1 = lim seq )

for seq being Real_Sequence st S1 = seq & seq is convergent holds

( S1 is convergent & lim S1 = lim seq )

proof end;

theorem Th27: :: TOPMETR4:23

for N being Subset of REAL

for M being Subset of R^1 st N = M holds

( ( for F being Subset-Family of REAL st F is Cover of N & ( for P being Subset of REAL st P in F holds

P is open ) holds

ex G being Subset-Family of REAL st

( G c= F & G is Cover of N & G is finite ) ) iff for F1 being Subset-Family of R^1 st F1 is Cover of M & F1 is open holds

ex G1 being Subset-Family of R^1 st

( G1 c= F1 & G1 is Cover of M & G1 is finite ) )

for M being Subset of R^1 st N = M holds

( ( for F being Subset-Family of REAL st F is Cover of N & ( for P being Subset of REAL st P in F holds

P is open ) holds

ex G being Subset-Family of REAL st

( G c= F & G is Cover of N & G is finite ) ) iff for F1 being Subset-Family of R^1 st F1 is Cover of M & F1 is open holds

ex G1 being Subset-Family of R^1 st

( G1 c= F1 & G1 is Cover of M & G1 is finite ) )

proof end;

theorem :: TOPMETR4:24

for N being Subset of REAL holds

( N is compact iff for F being Subset-Family of REAL st F is Cover of N & ( for P being Subset of REAL st P in F holds

P is open ) holds

ex G being Subset-Family of REAL st

( G c= F & G is Cover of N & G is finite ) )

( N is compact iff for F being Subset-Family of REAL st F is Cover of N & ( for P being Subset of REAL st P in F holds

P is open ) holds

ex G being Subset-Family of REAL st

( G c= F & G is Cover of N & G is finite ) )

proof end;

:: in JORDAN5A