:: Complete Spaces
:: by Karol P\c{a}k
::
:: Received October 12, 2007
:: Copyright (c) 2007-2018 Association of Mizar Users

definition
let M be non empty MetrStruct ;
let S be SetSequence of M;
attr S is pointwise_bounded means :Def1: :: COMPL_SP:def 1
for i being Nat holds S . i is bounded ;
end;

:: deftheorem Def1 defines pointwise_bounded COMPL_SP:def 1 :
for M being non empty MetrStruct
for S being SetSequence of M holds
( S is pointwise_bounded iff for i being Nat holds S . i is bounded );

registration
let M be non empty Reflexive MetrStruct ;
existence
ex b1 being SetSequence of M st
( b1 is pointwise_bounded & b1 is non-empty )
proof end;
end;

definition
let M be non empty Reflexive MetrStruct ;
let S be SetSequence of M;
func diameter S -> Real_Sequence means :Def2: :: COMPL_SP:def 2
for i being Nat holds it . i = diameter (S . i);
existence
ex b1 being Real_Sequence st
for i being Nat holds b1 . i = diameter (S . i)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Nat holds b1 . i = diameter (S . i) ) & ( for i being Nat holds b2 . i = diameter (S . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines diameter COMPL_SP:def 2 :
for M being non empty Reflexive MetrStruct
for S being SetSequence of M
for b3 being Real_Sequence holds
( b3 = diameter S iff for i being Nat holds b3 . i = diameter (S . i) );

theorem Th1: :: COMPL_SP:1
for M being non empty Reflexive MetrStruct
for S being pointwise_bounded SetSequence of M holds diameter S is bounded_below
proof end;

registration
let M be non empty Reflexive MetrStruct ;
let S be SetSequence of M;
coherence ;
end;

theorem Th2: :: COMPL_SP:2
for M being non empty Reflexive MetrStruct
for S being pointwise_bounded SetSequence of M st S is V176() holds
( diameter S is bounded_above & diameter S is non-increasing )
proof end;

theorem :: COMPL_SP:3
for M being non empty Reflexive MetrStruct
for S being pointwise_bounded SetSequence of M st S is V177() holds
diameter S is non-decreasing
proof end;

theorem Th4: :: COMPL_SP:4
for M being non empty Reflexive MetrStruct
for S being pointwise_bounded SetSequence of M st S is V176() & lim () = 0 holds
for F being sequence of M st ( for i being Nat holds F . i in S . i ) holds
F is Cauchy
proof end;

theorem Th5: :: COMPL_SP:5
for r being Real
for M being non empty Reflexive symmetric triangle MetrStruct
for p being Point of M st 0 <= r holds
diameter (cl_Ball (p,r)) <= 2 * r
proof end;

definition
let M be MetrStruct ;
let U be Subset of M;
attr U is open means :: COMPL_SP:def 3
U in Family_open_set M;
end;

:: deftheorem defines open COMPL_SP:def 3 :
for M being MetrStruct
for U being Subset of M holds
( U is open iff U in Family_open_set M );

definition
let M be MetrStruct ;
let A be Subset of M;
attr A is closed means :: COMPL_SP:def 4
A  is open ;
end;

:: deftheorem defines closed COMPL_SP:def 4 :
for M being MetrStruct
for A being Subset of M holds
( A is closed iff A  is open );

registration
let M be MetrStruct ;
cluster empty -> open for Subset of M;
coherence
for b1 being Subset of M st b1 is empty holds
b1 is open
proof end;
cluster empty -> closed for Subset of M;
coherence
for b1 being Subset of M st b1 is empty holds
b1 is closed
proof end;
end;

registration
let M be non empty MetrStruct ;
cluster non empty open for Subset of M;
existence
ex b1 being Subset of M st
( b1 is open & not b1 is empty )
proof end;
cluster non empty closed for Subset of M;
existence
ex b1 being Subset of M st
( b1 is closed & not b1 is empty )
proof end;
end;

theorem Th6: :: COMPL_SP:6
for M being MetrStruct
for A being Subset of M
for A9 being Subset of () st A9 = A holds
( ( A is open implies A9 is open ) & ( A9 is open implies A is open ) & ( A is closed implies A9 is closed ) & ( A9 is closed implies A is closed ) )
proof end;

definition
let T be TopStruct ;
let S be SetSequence of T;
attr S is open means :: COMPL_SP:def 5
for i being Nat holds S . i is open ;
attr S is closed means :Def6: :: COMPL_SP:def 6
for i being Nat holds S . i is closed ;
end;

:: deftheorem defines open COMPL_SP:def 5 :
for T being TopStruct
for S being SetSequence of T holds
( S is open iff for i being Nat holds S . i is open );

:: deftheorem Def6 defines closed COMPL_SP:def 6 :
for T being TopStruct
for S being SetSequence of T holds
( S is closed iff for i being Nat holds S . i is closed );

Lm1: for T being TopSpace ex S being SetSequence of T st
( S is open & S is closed & ( not T is empty implies S is non-empty ) )

proof end;

registration
let T be TopSpace;
existence
ex b1 being SetSequence of T st b1 is open
proof end;
existence
ex b1 being SetSequence of T st b1 is closed
proof end;
end;

registration
let T be non empty TopSpace;
existence
ex b1 being SetSequence of T st
( b1 is open & b1 is non-empty )
proof end;
existence
ex b1 being SetSequence of T st
( b1 is closed & b1 is non-empty )
proof end;
end;

definition
let M be MetrStruct ;
let S be SetSequence of M;
attr S is open means :: COMPL_SP:def 7
for i being Nat holds S . i is open ;
attr S is closed means :Def8: :: COMPL_SP:def 8
for i being Nat holds S . i is closed ;
end;

:: deftheorem defines open COMPL_SP:def 7 :
for M being MetrStruct
for S being SetSequence of M holds
( S is open iff for i being Nat holds S . i is open );

:: deftheorem Def8 defines closed COMPL_SP:def 8 :
for M being MetrStruct
for S being SetSequence of M holds
( S is closed iff for i being Nat holds S . i is closed );

registration
let M be non empty MetrSpace;
existence
ex b1 being SetSequence of M st
( b1 is non-empty & b1 is pointwise_bounded & b1 is open )
proof end;
existence
ex b1 being SetSequence of M st
( b1 is non-empty & b1 is pointwise_bounded & b1 is closed )
proof end;
end;

theorem Th7: :: COMPL_SP:7
for M being MetrStruct
for S being SetSequence of M
for S9 being SetSequence of () st S9 = S holds
( ( S is open implies S9 is open ) & ( S9 is open implies S is open ) & ( S is closed implies S9 is closed ) & ( S9 is closed implies S is closed ) )
proof end;

theorem Th8: :: COMPL_SP:8
for M being non empty Reflexive symmetric triangle MetrStruct
for S, CL being Subset of M st S is bounded holds
for S9 being Subset of () st S = S9 & CL = Cl S9 holds
( CL is bounded & diameter S = diameter CL )
proof end;

theorem Th9: :: COMPL_SP:9
for M being non empty MetrSpace
for C being sequence of M ex S being non-empty closed SetSequence of M st
( S is V176() & ( C is Cauchy implies ( S is pointwise_bounded & lim () = 0 ) ) & ( for i being Nat ex U being Subset of () st
( U = { (C . j) where j is Nat : j >= i } & S . i = Cl U ) ) )
proof end;

theorem Th10: :: COMPL_SP:10
for M being non empty MetrSpace holds
( M is complete iff for S being non-empty pointwise_bounded closed SetSequence of M st S is V176() & lim () = 0 holds
not meet S is empty )
proof end;

theorem Th11: :: COMPL_SP:11
for T being non empty TopSpace
for S being non-empty SetSequence of T st S is V176() holds
for F being Subset-Family of T st F = rng S holds
F is centered
proof end;

theorem Th12: :: COMPL_SP:12
for M being non empty MetrStruct
for S being SetSequence of M
for F being Subset-Family of () st F = rng S holds
( ( S is open implies F is open ) & ( S is closed implies F is closed ) )
proof end;

theorem Th13: :: COMPL_SP:13
for T being non empty TopSpace
for F being Subset-Family of T
for S being SetSequence of T st rng S c= F holds
ex R being SetSequence of T st
( R is V176() & ( F is centered implies R is non-empty ) & ( F is open implies R is open ) & ( F is closed implies R is closed ) & ( for i being Nat holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )
proof end;

theorem :: COMPL_SP:14
for M being non empty MetrSpace holds
( M is complete iff for F being Subset-Family of () st F is closed & F is centered & ( for r being Real st r > 0 holds
ex A being Subset of M st
( A in F & A is bounded & diameter A < r ) ) holds
not meet F is empty )
proof end;

theorem Th15: :: COMPL_SP:15
for M being non empty MetrSpace
for A being non empty Subset of M
for B being Subset of M
for B9 being Subset of (M | A) st B = B9 holds
( B9 is bounded iff B is bounded )
proof end;

theorem Th16: :: COMPL_SP:16
for M being non empty MetrSpace
for A being non empty Subset of M
for B being Subset of M
for B9 being Subset of (M | A) st B = B9 & B is bounded holds
diameter B9 <= diameter B
proof end;

theorem Th17: :: COMPL_SP:17
for M being non empty MetrSpace
for A being non empty Subset of M
for S being sequence of (M | A) holds S is sequence of M
proof end;

theorem Th18: :: COMPL_SP:18
for M being non empty MetrSpace
for A being non empty Subset of M
for S being sequence of (M | A)
for S9 being sequence of M st S = S9 holds
( S9 is Cauchy iff S is Cauchy )
proof end;

theorem :: COMPL_SP:19
for M being non empty MetrSpace st M is complete holds
for A being non empty Subset of M
for A9 being Subset of () st A = A9 holds
( M | A is complete iff A9 is closed )
proof end;

definition
let T be TopStruct ;
attr T is countably_compact means :: COMPL_SP:def 9
for F being Subset-Family of T st F is Cover of T & F is open & F is countable holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite );
end;

:: deftheorem defines countably_compact COMPL_SP:def 9 :
for T being TopStruct holds
( T is countably_compact iff for F being Subset-Family of T st F is Cover of T & F is open & F is countable holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite ) );

theorem :: COMPL_SP:20
for T being TopStruct st T is compact holds
T is countably_compact ;

theorem Th21: :: COMPL_SP:21
for T being non empty TopSpace holds
( T is countably_compact iff for F being Subset-Family of T st F is centered & F is closed & F is countable holds
meet F <> {} )
proof end;

theorem Th22: :: COMPL_SP:22
for T being non empty TopSpace holds
( T is countably_compact iff for S being non-empty closed SetSequence of T st S is V176() holds
meet S <> {} )
proof end;

theorem Th23: :: COMPL_SP:23
for T being non empty TopSpace
for F being Subset-Family of T
for S being SetSequence of T st rng S c= F & S is non-empty holds
ex R being non-empty closed SetSequence of T st
( R is V176() & ( F is locally_finite & S is one-to-one implies meet R = {} ) & ( for i being Nat ex Si being Subset-Family of T st
( R . i = Cl (union Si) & Si = { (S . j) where j is Element of NAT : j >= i } ) ) )
proof end;

Lm2: for T being non empty TopSpace st T is countably_compact holds
for F being Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds
F is finite

proof end;

Lm3: for T being non empty TopSpace st ( for F being Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds
F is finite ) holds
for F being Subset-Family of T st F is locally_finite & ( for A being Subset of T st A in F holds
card A = 1 ) holds
F is finite

proof end;

Lm4: for T being non empty TopSpace st ( for F being Subset-Family of T st F is locally_finite & ( for A being Subset of T st A in F holds
card A = 1 ) holds
F is finite ) holds
for A being Subset of T st A is infinite holds
not Der A is empty

proof end;

theorem :: COMPL_SP:24
canceled;

::\$CT
theorem Th24: :: COMPL_SP:25
for X being non empty set
for F being SetSequence of X st F is V176() holds
for S being sequence of X st ( for n being Nat holds S . n in F . n ) & rng S is finite holds
not meet F is empty
proof end;

Lm5: for T being non empty T_1 TopSpace st ( for A being Subset of T st A is infinite & A is countable holds
not Der A is empty ) holds
T is countably_compact

proof end;

Lm6: for T being non empty TopSpace st ( for F being Subset-Family of T st F is locally_finite & ( for A being Subset of T st A in F holds
card A = 1 ) holds
F is finite ) holds
T is countably_compact

proof end;

theorem Th25: :: COMPL_SP:26
for T being non empty TopSpace holds
( T is countably_compact iff for F being Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds
F is finite )
proof end;

theorem Th26: :: COMPL_SP:27
for T being non empty TopSpace holds
( T is countably_compact iff for F being Subset-Family of T st F is locally_finite & ( for A being Subset of T st A in F holds
card A = 1 ) holds
F is finite )
proof end;

theorem Th27: :: COMPL_SP:28
for T being non empty T_1 TopSpace holds
( T is countably_compact iff for A being Subset of T st A is infinite holds
not Der A is empty )
proof end;

theorem :: COMPL_SP:29
for T being non empty T_1 TopSpace holds
( T is countably_compact iff for A being Subset of T st A is infinite & A is countable holds
not Der A is empty ) by ;

scheme :: COMPL_SP:sch 1
Th39{ F1() -> non empty set , P1[ set , set ] } :
ex A being Subset of F1() st
( ( for x, y being Element of F1() st x in A & y in A & x <> y holds
P1[x,y] ) & ( for x being Element of F1() ex y being Element of F1() st
( y in A & P1[x,y] ) ) )
provided
A1: for x, y being Element of F1() holds
( P1[x,y] iff P1[y,x] ) and
A2: for x being Element of F1() holds P1[x,x]
proof end;

scheme :: COMPL_SP:sch 2
Th39{ F1() -> non empty set , P1[ set , set ] } :
ex A being Subset of F1() st
( ( for x, y being Element of F1() st x in A & y in A & x <> y holds
P1[x,y] ) & ( for x being Element of F1() ex y being Element of F1() st
( y in A & P1[x,y] ) ) )
provided
A1: for x, y being Element of F1() holds
( P1[x,y] iff P1[y,x] ) and
A2: for x being Element of F1() holds P1[x,x]
proof end;

theorem Th29: :: COMPL_SP:30
for M being non empty Reflexive symmetric MetrStruct
for r being Real st r > 0 holds
ex A being Subset of M st
( ( for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ) & ( for p being Point of M ex q being Point of M st
( q in A & p in Ball (q,r) ) ) )
proof end;

theorem Th30: :: COMPL_SP:31
for M being non empty Reflexive symmetric triangle MetrStruct holds
( M is totally_bounded iff for r being Real
for A being Subset of M st r > 0 & ( for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ) holds
A is finite )
proof end;

Lm7: for M being non empty Reflexive symmetric triangle MetrStruct
for r being Real
for A being Subset of M st r > 0 & ( for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ) holds
for F being Subset-Family of () st F = { {x} where x is Element of () : x in A } holds
F is locally_finite

proof end;

theorem Th31: :: COMPL_SP:32
for M being non empty Reflexive symmetric triangle MetrStruct st TopSpaceMetr M is countably_compact holds
M is totally_bounded
proof end;

theorem Th32: :: COMPL_SP:33
for M being non empty MetrSpace st M is totally_bounded holds
TopSpaceMetr M is second-countable
proof end;

theorem Th33: :: COMPL_SP:34
for T being non empty TopSpace st T is second-countable holds
for F being Subset-Family of T st F is Cover of T & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable )
proof end;

theorem Th34: :: COMPL_SP:35
for M being non empty MetrSpace holds
( TopSpaceMetr M is compact iff TopSpaceMetr M is countably_compact )
proof end;

theorem Th35: :: COMPL_SP:36
for X being set
for F being Subset-Family of X st F is finite holds
for A being Subset of X st A is infinite & A c= union F holds
ex Y being Subset of X st
( Y in F & Y /\ A is infinite )
proof end;

theorem :: COMPL_SP:37
for M being non empty MetrSpace holds
( TopSpaceMetr M is compact iff ( M is totally_bounded & M is complete ) )
proof end;

theorem Th37: :: COMPL_SP:38
for X being set
for M being MetrStruct
for a being Point of M
for x being set holds
( x in [:X,( the carrier of M \ {a}):] \/ {[X,a]} iff ex y being set ex b being Point of M st
( x = [y,b] & ( ( y in X & b <> a ) or ( y = X & b = a ) ) ) )
proof end;

definition
let M be MetrStruct ;
let a be Point of M;
let X be set ;
func well_dist (a,X) -> Function of [:([:X,( the carrier of M \ {a}):] \/ {[X,a]}),([:X,( the carrier of M \ {a}):] \/ {[X,a]}):],REAL means :Def10: :: COMPL_SP:def 10
for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being object
for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds
( ( x1 = y1 implies it . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies it . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) );
existence
ex b1 being Function of [:([:X,( the carrier of M \ {a}):] \/ {[X,a]}),([:X,( the carrier of M \ {a}):] \/ {[X,a]}):],REAL st
for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being object
for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds
( ( x1 = y1 implies b1 . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies b1 . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) )
proof end;
uniqueness
for b1, b2 being Function of [:([:X,( the carrier of M \ {a}):] \/ {[X,a]}),([:X,( the carrier of M \ {a}):] \/ {[X,a]}):],REAL st ( for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being object
for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds
( ( x1 = y1 implies b1 . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies b1 . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) ) & ( for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being object
for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds
( ( x1 = y1 implies b2 . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies b2 . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines well_dist COMPL_SP:def 10 :
for M being MetrStruct
for a being Point of M
for X being set
for b4 being Function of [:([:X,( the carrier of M \ {a}):] \/ {[X,a]}),([:X,( the carrier of M \ {a}):] \/ {[X,a]}):],REAL holds
( b4 = well_dist (a,X) iff for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being object
for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds
( ( x1 = y1 implies b4 . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies b4 . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) );

theorem :: COMPL_SP:39
for M being MetrStruct
for a being Point of M
for X being non empty set holds
( ( well_dist (a,X) is Reflexive implies M is Reflexive ) & ( well_dist (a,X) is symmetric implies M is symmetric ) & ( well_dist (a,X) is triangle & well_dist (a,X) is Reflexive implies M is triangle ) & ( well_dist (a,X) is discerning & well_dist (a,X) is Reflexive implies M is discerning ) )
proof end;

definition
let M be MetrStruct ;
let a be Point of M;
let X be set ;
func WellSpace (a,X) -> strict MetrStruct equals :: COMPL_SP:def 11
MetrStruct(# ([:X,( the carrier of M \ {a}):] \/ {[X,a]}),(well_dist (a,X)) #);
coherence
MetrStruct(# ([:X,( the carrier of M \ {a}):] \/ {[X,a]}),(well_dist (a,X)) #) is strict MetrStruct
;
end;

:: deftheorem defines WellSpace COMPL_SP:def 11 :
for M being MetrStruct
for a being Point of M
for X being set holds WellSpace (a,X) = MetrStruct(# ([:X,( the carrier of M \ {a}):] \/ {[X,a]}),(well_dist (a,X)) #);

registration
let M be MetrStruct ;
let a be Point of M;
let X be set ;
cluster WellSpace (a,X) -> non empty strict ;
coherence
not WellSpace (a,X) is empty
;
end;

Lm8: for M being MetrStruct
for a being Point of M
for X being set holds
( ( M is Reflexive implies WellSpace (a,X) is Reflexive ) & ( M is symmetric implies WellSpace (a,X) is symmetric ) & ( M is triangle & M is symmetric & M is Reflexive implies WellSpace (a,X) is triangle ) & ( M is triangle & M is symmetric & M is Reflexive & M is discerning implies WellSpace (a,X) is discerning ) )

proof end;

registration
let M be Reflexive MetrStruct ;
let a be Point of M;
let X be set ;
cluster WellSpace (a,X) -> strict Reflexive ;
coherence
WellSpace (a,X) is Reflexive
by Lm8;
end;

registration
let M be symmetric MetrStruct ;
let a be Point of M;
let X be set ;
cluster WellSpace (a,X) -> strict symmetric ;
coherence
WellSpace (a,X) is symmetric
by Lm8;
end;

registration
let M be Reflexive symmetric triangle MetrStruct ;
let a be Point of M;
let X be set ;
cluster WellSpace (a,X) -> strict triangle ;
coherence
WellSpace (a,X) is triangle
by Lm8;
end;

registration
let M be MetrSpace;
let a be Point of M;
let X be set ;
cluster WellSpace (a,X) -> strict discerning ;
coherence
WellSpace (a,X) is discerning
by Lm8;
end;

theorem :: COMPL_SP:40
for M being non empty Reflexive triangle MetrStruct
for a being Point of M
for X being non empty set st WellSpace (a,X) is complete holds
M is complete
proof end;

theorem Th40: :: COMPL_SP:41
for X being set
for M being non empty Reflexive symmetric triangle MetrStruct
for a being Point of M
for S being sequence of (WellSpace (a,X)) holds
( not S is Cauchy or for Xa being Point of (WellSpace (a,X)) st Xa = [X,a] holds
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist ((S . m),Xa) < r or ex n being Nat ex Y being set st
for m being Nat st m >= n holds
ex p being Point of M st S . m = [Y,p] )
proof end;

theorem Th41: :: COMPL_SP:42
for X being set
for M being non empty Reflexive symmetric triangle MetrStruct
for a being Point of M st M is complete holds
WellSpace (a,X) is complete
proof end;

theorem Th42: :: COMPL_SP:43
for M being non empty Reflexive symmetric triangle MetrStruct st M is complete holds
for a being Point of M st ex b being Point of M st dist (a,b) <> 0 holds
for X being infinite set holds
( WellSpace (a,X) is complete & ex S being non-empty pointwise_bounded SetSequence of (WellSpace (a,X)) st
( S is closed & S is V176() & meet S is empty ) )
proof end;

theorem :: COMPL_SP:44
ex M being non empty MetrSpace st
( M is complete & ex S being non-empty pointwise_bounded SetSequence of M st
( S is closed & S is V176() & meet S is empty ) )
proof end;