TOPMETR4: Compactness in Metric Spaces

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 :

registration

let M be non empty MetrSpace;

cluster empty -> sequentially_compact for Element of K19( the carrier of M);

coherence by Th6;

end;

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;

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;

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;