let T be non empty Reflexive symmetric triangle MetrStruct ; ( 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 5;
assume A2:
TopSpaceMetr T is compact
; T is complete
let S2 be sequence of T; TBSP_1:def 5 ( S2 is Cauchy implies S2 is convergent )
assume A3:
S2 is Cauchy
; S2 is convergent
S2 is convergent
proof
A4:
for
p being
Nat holds
{ x where x is Point of T : ex n being Nat st
( p <= n & x = S2 . n ) } <> {}
proof
let p be
Nat;
{ x where x is Point of T : ex n being Nat st
( p <= n & x = S2 . n ) } <> {}
S2 . p in { x where x is Point of T : ex n being Nat st
( p <= n & x = S2 . n ) }
;
hence
{ x where x is Point of T : ex n being Nat st
( p <= n & x = S2 . n ) } <> {}
;
verum
end;
defpred S1[
Subset of
(TopSpaceMetr T)]
means ex
p being
Nat st $1
= { x where x is Point of T : ex n being Nat st
( p <= n & x = S2 . n ) } ;
consider F being
Subset-Family of
(TopSpaceMetr T) such that A5:
for
B being
Subset of
(TopSpaceMetr T) holds
(
B in F iff
S1[
B] )
from SUBSET_1:sch 3();
defpred S2[
Point of
T]
means ex
n being
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, A5;
reconsider B0 =
{ x where x is Point of T : S2[x] } as
Subset of
(TopSpaceMetr T) by A1, A6;
reconsider F =
F as
Subset-Family of
(TopSpaceMetr T) ;
set G =
clf F;
A8:
Cl B0 in clf F
by A7, PCOMPS_1:def 2;
A9:
clf F is
centered
proof
thus
clf F <> {}
by A8;
FINSET_1:def 3 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 ;
( 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
;
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 ;
ORDINAL1:def 8 ( not B in H or not C in H or B,C are_c=-comparable )
assume that A14:
B in H
and A15:
C in H
;
B,C are_c=-comparable
reconsider B =
B,
C =
C as
Subset of
(TopSpaceMetr T) by A13, A14, A15;
consider V being
Subset of
(TopSpaceMetr T) such that A16:
B = Cl V
and A17:
V in F
by A11, A14, PCOMPS_1:def 2;
consider p being
Nat such that A18:
V = { x where x is Point of T : ex n being Nat st
( p <= n & x = S2 . n ) }
by A5, A17;
consider W being
Subset of
(TopSpaceMetr T) such that A19:
C = Cl W
and A20:
W in F
by A11, A15, PCOMPS_1:def 2;
consider q being
Nat such that A21:
W = { x where x is Point of T : ex n being Nat st
( q <= n & x = S2 . n ) }
by A5, A20;
then
(
B c= C or
C c= B )
by A16, A19, PRE_TOPC:19;
hence
B,
C are_c=-comparable
;
verum
end;
then consider m being
set such that A32:
m in H
and A33:
for
C being
set st
C in H holds
m c= C
by A10, A12, FINSET_1:11;
A34:
m c= meet H
by A10, A33, SETFAM_1:5;
reconsider m =
m as
Subset of
(TopSpaceMetr T) by A13, A32;
consider A being
Subset of
(TopSpaceMetr T) such that A35:
m = Cl A
and A36:
A in F
by A11, A32, PCOMPS_1:def 2;
A <> {}
by A5, A4, A36;
then
m <> {}
by A35, PRE_TOPC:18, XBOOLE_1:3;
hence
not
meet H = {}
by A34;
verum
end;
clf F is
closed
by PCOMPS_1:11;
then
meet (clf F) <> {}
by A2, A9, COMPTS_1:4;
then consider c being
Point of
(TopSpaceMetr T) such that A37:
c in meet (clf F)
by SUBSET_1:4;
reconsider c =
c as
Point of
T by A1;
take
c
;
TBSP_1:def 2 for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S2 . m),c) < r
let r be
Real;
( r > 0 implies ex n being Nat st
for m being Nat st n <= m holds
dist ((S2 . m),c) < r )
assume
0 < r
;
ex n being Nat st
for m being Nat st n <= m holds
dist ((S2 . m),c) < r
then A38:
0 < r / 2
by XREAL_1:215;
then consider p being
Nat such that A39:
for
n,
m being
Nat st
p <= n &
p <= m holds
dist (
(S2 . n),
(S2 . m))
< r / 2
by A3;
dist (
c,
c)
< r / 2
by A38, METRIC_1:1;
then A40:
c in Ball (
c,
(r / 2))
by METRIC_1:11;
reconsider Z =
Ball (
c,
(r / 2)) as
Subset of
(TopSpaceMetr T) by A1;
Ball (
c,
(r / 2))
in Family_open_set T
by PCOMPS_1:29;
then A41:
Z is
open
by A1, PRE_TOPC:def 2;
defpred S3[
set ]
means ex
n being
Nat st
(
p <= n & $1
= S2 . n );
set B =
{ x where x is Point of T : S3[x] } ;
A42:
{ x where x is Point of T : S3[x] } is
Subset of
T
from DOMAIN_1:sch 7();
then A43:
{ x where x is Point of T : S3[x] } in F
by A1, A5;
reconsider B =
{ x where x is Point of T : S3[x] } as
Subset of
(TopSpaceMetr T) by A1, A42;
Cl B in clf F
by A43, PCOMPS_1:def 2;
then
c in Cl B
by A37, SETFAM_1:def 1;
then
B meets Z
by A40, A41, PRE_TOPC:def 7;
then consider g being
object such that A44:
g in B /\ Z
by XBOOLE_0:4;
take
p
;
for m being Nat st p <= m holds
dist ((S2 . m),c) < r
let m be
Nat;
( p <= m implies dist ((S2 . m),c) < r )
A45:
g in B
by A44, XBOOLE_0:def 4;
A46:
g in Z
by A44, XBOOLE_0:def 4;
then reconsider g =
g as
Point of
T ;
consider x being
Point of
T such that A47:
g = x
and A48:
ex
n being
Nat st
(
p <= n &
x = S2 . n )
by A45;
consider n being
Nat such that A49:
p <= n
and A50:
x = S2 . n
by A48;
assume
p <= m
;
dist ((S2 . m),c) < r
then A51:
dist (
(S2 . m),
(S2 . n))
< r / 2
by A39, A49;
dist (
(S2 . n),
c)
< r / 2
by A46, A47, A50, METRIC_1:11;
then A52:
(dist ((S2 . m),(S2 . n))) + (dist ((S2 . n),c)) < (r / 2) + (r / 2)
by A51, XREAL_1:8;
dist (
(S2 . m),
c)
<= (dist ((S2 . m),(S2 . n))) + (dist ((S2 . n),c))
by METRIC_1:4;
hence
dist (
(S2 . m),
c)
< r
by A52, XXREAL_0:2;
verum
end;
hence
S2 is convergent
; verum