:: Complete Spaces
:: by Karol P\c{a}k
::
:: Received October 12, 2007
:: Copyright (c) 2007-2021 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 ;

cluster Relation-like non-empty omega -defined bool the carrier of M -valued non empty Function-like total V29( omega , bool the carrier of M) pointwise_bounded for Element of bool [:omega,(bool the carrier of M):];

existence
ex b₁ being SetSequence of M st
( b₁ is pointwise_bounded & b₁ 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 b₁ being Real_Sequence st
for i being Nat holds b₁ . i = diameter (S . i)

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for i being Nat holds b₁ . i = diameter (S . i) ) & ( for i being Nat holds b₂ . i = diameter (S . i) ) holds
b₁ = b₂

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 b₃ being Real_Sequence holds
( b₃ = diameter S iff for i being Nat holds b₃ . 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;

cluster diameter S -> real-valued ;

coherence
diameter S is real-valued ;

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 (diameter S) = 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 Element of bool the carrier of M;

coherence
for b₁ being Subset of M st b₁ is empty holds
b₁ is open

proof end;

cluster empty -> closed for Element of bool the carrier of M;

coherence
for b₁ being Subset of M st b₁ is empty holds
b₁ is closed

proof end;

end;

registration

let M be non empty MetrStruct ;

cluster non empty open for Element of bool the carrier of M;

existence
ex b₁ being Subset of M st
( b₁ is open & not b₁ is empty )

proof end;

cluster non empty closed for Element of bool the carrier of M;

existence
ex b₁ being Subset of M st
( b₁ is closed & not b₁ 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 (TopSpaceMetr M) 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;

cluster Relation-like omega -defined bool the carrier of T -valued non empty Function-like total V29( omega , bool the carrier of T) open for Element of bool [:omega,(bool the carrier of T):];

existence
ex b₁ being SetSequence of T st b₁ is open

proof end;

cluster Relation-like omega -defined bool the carrier of T -valued non empty Function-like total V29( omega , bool the carrier of T) closed for Element of bool [:omega,(bool the carrier of T):];

existence
ex b₁ being SetSequence of T st b₁ is closed

proof end;

end;

registration

let T be non empty TopSpace;

cluster Relation-like non-empty omega -defined bool the carrier of T -valued non empty Function-like total V29( omega , bool the carrier of T) open for Element of bool [:omega,(bool the carrier of T):];

existence
ex b₁ being SetSequence of T st
( b₁ is open & b₁ is non-empty )

proof end;

cluster Relation-like non-empty omega -defined bool the carrier of T -valued non empty Function-like total V29( omega , bool the carrier of T) closed for Element of bool [:omega,(bool the carrier of T):];

existence
ex b₁ being SetSequence of T st
( b₁ is closed & b₁ 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;

cluster Relation-like non-empty omega -defined bool the carrier of M -valued non empty Function-like total V29( omega , bool the carrier of M) pointwise_bounded open for Element of bool [:omega,(bool the carrier of M):];

existence
ex b₁ being SetSequence of M st
( b₁ is non-empty & b₁ is pointwise_bounded & b₁ is open )

proof end;

cluster Relation-like non-empty omega -defined bool the carrier of M -valued non empty Function-like total V29( omega , bool the carrier of M) pointwise_bounded closed for Element of bool [:omega,(bool the carrier of M):];

existence
ex b₁ being SetSequence of M st
( b₁ is non-empty & b₁ is pointwise_bounded & b₁ 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 (TopSpaceMetr M) 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 (TopSpaceMetr M) 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 (diameter S) = 0 ) ) & ( for i being Nat ex U being Subset of (TopSpaceMetr M) 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 (diameter S) = 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 (TopSpaceMetr M) 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 (TopSpaceMetr M) 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 (TopSpaceMetr M) 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 Lm5, Th27;

scheme :: COMPL_SP:sch 1
Th39{ F₁() -> non empty set , P₁[ set , set ] } :

ex A being Subset of F₁() st
( ( for x, y being Element of F₁() st x in A & y in A & x <> y holds
P₁[x,y] ) & ( for x being Element of F₁() ex y being Element of F₁() st
( y in A & P₁[x,y] ) ) )

provided

A1: for x, y being Element of F₁() holds
( P₁[x,y] iff P₁[y,x] ) and
A2: for x being Element of F₁() holds P₁[x,x]

proof end;

scheme :: COMPL_SP:sch 2
Th39{ F₁() -> non empty set , P₁[ set , set ] } :

ex A being Subset of F₁() st
( ( for x, y being Element of F₁() st x in A & y in A & x <> y holds
P₁[x,y] ) & ( for x being Element of F₁() ex y being Element of F₁() st
( y in A & P₁[x,y] ) ) )

provided

A1: for x, y being Element of F₁() holds
( P₁[x,y] iff P₁[y,x] ) and
A2: for x being Element of F₁() holds P₁[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 (TopSpaceMetr M) st F = { {x} where x is Element of (TopSpaceMetr M) : 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 b₁ 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 b₁ . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies b₁ . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) )

proof end;

uniqueness
for b₁, b₂ 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 b₁ . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies b₁ . (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 b₂ . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies b₂ . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) ) holds
b₁ = b₂

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 b₄ being Function of [:([:X,( the carrier of M \ {a}):] \/ {[X,a]}),([:X,( the carrier of M \ {a}):] \/ {[X,a]}):],REAL holds
( b₄ = 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 b₄ . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies b₄ . (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;