:: Compactness in Metric Spaces
:: by Kazuhisa Nakasho , Keiko Narita and Yasunari Shidama
::
:: Received June 30, 2016
:: Copyright (c) 2016-2021 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 )
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
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 )
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) )
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 ) )
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 )
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) ) )
proof end;

definition
let M be non empty MetrSpace;
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 );
end;

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

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;
cluster empty -> sequentially_compact for Element of K19( the carrier of M);
coherence
for b1 being Subset of M st b1 is empty holds
b1 is sequentially_compact
by Th6;
end;

definition
let M be non empty MetrSpace;
attr M is sequentially_compact means :: TOPMETR4:def 2
[#] M is sequentially_compact ;
end;

:: deftheorem defines sequentially_compact TOPMETR4:def 2 :
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} )
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
proof end;

theorem :: TOPMETR4:10
for M being non empty MetrSpace st M is sequentially_compact holds
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 Th11: :: TOPMETR4:11
for M being non empty MetrSpace holds
( TopSpaceMetr M is compact iff M is sequentially_compact )
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 )
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 )
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 )
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 )
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 )
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 )
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 )
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 )
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 )
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 ) )
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 )
proof end;

:: The equivalence of the notions of compactness in R^1 and REAL was shown
:: in JORDAN5A
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 ) )
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 ) )
proof end;