let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: ( TopSpaceMetr T is compact implies T is complete )
set TM = TopSpaceMetr T;
A1:
TopSpaceMetr T = TopStruct(# the carrier of T,(Family_open_set T) #)
by PCOMPS_1:def 6;
assume A2:
TopSpaceMetr T is compact
; :: thesis: T is complete
let S2 be sequence of T; :: according to TBSP_1:def 6 :: thesis: ( S2 is Cauchy implies S2 is convergent )
assume A3:
S2 is Cauchy
; :: thesis: S2 is convergent
S2 is convergent
proof
defpred S1[
Subset of
(TopSpaceMetr T)]
means ex
p being
Element of
NAT st $1
= { x where x is Point of T : ex n being Element of NAT st
( p <= n & x = S2 . n ) } ;
consider F being
Subset-Family of
(TopSpaceMetr T) such that A4:
for
B being
Subset of
(TopSpaceMetr T) holds
(
B in F iff
S1[
B] )
from SUBSET_1:sch 3();
A5:
for
p being
Element of
NAT holds
{ x where x is Point of T : ex n being Element of NAT st
( p <= n & x = S2 . n ) } <> {}
defpred S2[
Point of
T]
means ex
n being
Element of
NAT st
(
0 <= n & $1
= S2 . n );
set B0 =
{ x where x is Point of T : S2[x] } ;
A6:
{ x where x is Point of T : S2[x] } is
Subset of
T
from DOMAIN_1:sch 7();
then A7:
{ x where x is Point of T : S2[x] } in F
by A1, A4;
reconsider F =
F as
Subset-Family of
(TopSpaceMetr T) ;
set G =
clf F;
reconsider B0 =
{ x where x is Point of T : S2[x] } as
Subset of
(TopSpaceMetr T) by A1, A6;
A8:
Cl B0 in clf F
by A7, PCOMPS_1:def 3;
A9:
clf F is
closed
by PCOMPS_1:14;
clf F is
centered
proof
thus
clf F <> {}
by A8;
:: according to FINSET_1:def 3 :: thesis: for b1 being set holds
( b1 = {} or not b1 c= clf F or not b1 is finite or not meet b1 = {} )
let H be
set ;
:: thesis: ( H = {} or not H c= clf F or not H is finite or not meet H = {} )
assume that A10:
H <> {}
and A11:
H c= clf F
and A12:
H is
finite
;
:: thesis: not meet H = {}
A13:
H c= bool the
carrier of
(TopSpaceMetr T)
by A11, XBOOLE_1:1;
H is
c=-linear
proof
let B,
C be
set ;
:: according to ORDINAL1:def 9 :: thesis: ( not B in H or not C in H or not R7(B,C) )
assume A14:
(
B in H &
C in H )
;
:: thesis: R7(B,C)
then reconsider B =
B,
C =
C as
Subset of
(TopSpaceMetr T) by A13;
consider V being
Subset of
(TopSpaceMetr T) such that A15:
(
B = Cl V &
V in F )
by A11, A14, PCOMPS_1:def 3;
consider W being
Subset of
(TopSpaceMetr T) such that A16:
(
C = Cl W &
W in F )
by A11, A14, PCOMPS_1:def 3;
consider p being
Element of
NAT such that A17:
V = { x where x is Point of T : ex n being Element of NAT st
( p <= n & x = S2 . n ) }
by A4, A15;
consider q being
Element of
NAT such that A18:
W = { x where x is Point of T : ex n being Element of NAT st
( q <= n & x = S2 . n ) }
by A4, A16;
(
V c= W or
W c= V )
then
(
B c= C or
C c= B )
by A15, A16, PRE_TOPC:49;
hence
R7(
B,
C)
by XBOOLE_0:def 9;
:: thesis: verum
end;
then consider m being
set such that A25:
m in H
and A26:
for
C being
set st
C in H holds
m c= C
by A10, A12, FINSET_1:30;
A27:
m c= meet H
by A10, A26, SETFAM_1:6;
reconsider m =
m as
Subset of
(TopSpaceMetr T) by A13, A25;
consider A being
Subset of
(TopSpaceMetr T) such that A28:
(
m = Cl A &
A in F )
by A11, A25, PCOMPS_1:def 3;
A <> {}
by A4, A5, A28;
then
m <> {}
by A28, PRE_TOPC:48, XBOOLE_1:3;
hence
not
meet H = {}
by A27;
:: thesis: verum
end;
then
meet (clf F) <> {}
by A2, A9, COMPTS_1:13;
then consider c being
Point of
(TopSpaceMetr T) such that A29:
c in meet (clf F)
by SUBSET_1:10;
reconsider c =
c as
Point of
T by A1;
take
c
;
:: according to TBSP_1:def 3 :: thesis: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S2 . m),c < r
let r be
Real;
:: thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S2 . m),c < r )
assume
0 < r
;
:: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S2 . m),c < r
then A30:
0 < r / 2
by XREAL_1:217;
then consider p being
Element of
NAT such that A31:
for
n,
m being
Element of
NAT st
p <= n &
p <= m holds
dist (S2 . n),
(S2 . m) < r / 2
by A3, Def5;
defpred S3[
set ]
means ex
n being
Element of
NAT st
(
p <= n & $1
= S2 . n );
set B =
{ x where x is Point of T : S3[x] } ;
A32:
{ x where x is Point of T : S3[x] } is
Subset of
T
from DOMAIN_1:sch 7();
then A33:
{ x where x is Point of T : S3[x] } in F
by A1, A4;
reconsider B =
{ x where x is Point of T : S3[x] } as
Subset of
(TopSpaceMetr T) by A1, A32;
Cl B in clf F
by A33, PCOMPS_1:def 3;
then A34:
c in Cl B
by A29, SETFAM_1:def 1;
dist c,
c < r / 2
by A30, METRIC_1:1;
then A35:
c in Ball c,
(r / 2)
by METRIC_1:12;
A36:
Ball c,
(r / 2) in Family_open_set T
by PCOMPS_1:33;
reconsider Z =
Ball c,
(r / 2) as
Subset of
(TopSpaceMetr T) by A1;
Z is
open
by A1, A36, PRE_TOPC:def 5;
then
B meets Z
by A34, A35, PRE_TOPC:def 13;
then consider g being
set such that A37:
g in B /\ Z
by XBOOLE_0:4;
A38:
(
g in B &
g in Z )
by A37, XBOOLE_0:def 4;
then reconsider g =
g as
Point of
T ;
consider x being
Point of
T such that A39:
(
g = x & ex
n being
Element of
NAT st
(
p <= n &
x = S2 . n ) )
by A38;
consider n being
Element of
NAT such that A40:
(
p <= n &
x = S2 . n )
by A39;
A41:
dist (S2 . n),
c < r / 2
by A38, A39, A40, METRIC_1:12;
take
p
;
:: thesis: for m being Element of NAT st p <= m holds
dist (S2 . m),c < r
let m be
Element of
NAT ;
:: thesis: ( p <= m implies dist (S2 . m),c < r )
assume
p <= m
;
:: thesis: dist (S2 . m),c < r
then
dist (S2 . m),
(S2 . n) < r / 2
by A31, A40;
then A42:
(dist (S2 . m),(S2 . n)) + (dist (S2 . n),c) < (r / 2) + (r / 2)
by A41, XREAL_1:10;
dist (S2 . m),
c <= (dist (S2 . m),(S2 . n)) + (dist (S2 . n),c)
by METRIC_1:4;
hence
dist (S2 . m),
c < r
by A42, XXREAL_0:2;
:: thesis: verum
end;
hence
S2 is convergent
; :: thesis: verum