:: by Karol P\c{a}k

::

:: Received October 12, 2007

:: Copyright (c) 2007-2019 Association of Mizar Users

:: 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 );

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 ;

ex b_{1} being SetSequence of M st

( b_{1} is pointwise_bounded & b_{1} is non-empty )

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 for Element of bool [:omega,(bool the carrier of M):];

existence ex b

( b

proof end;

definition

let M be non empty Reflexive MetrStruct ;

let S be SetSequence of M;

ex b_{1} being Real_Sequence st

for i being Nat holds b_{1} . i = diameter (S . i)

for b_{1}, b_{2} being Real_Sequence st ( for i being Nat holds b_{1} . i = diameter (S . i) ) & ( for i being Nat holds b_{2} . i = diameter (S . i) ) holds

b_{1} = b_{2}

end;
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 for i being Nat holds it . i = diameter (S . i);

ex b

for i being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines diameter COMPL_SP:def 2 :

for M being non empty Reflexive MetrStruct

for S being SetSequence of M

for b_{3} being Real_Sequence holds

( b_{3} = diameter S iff for i being Nat holds b_{3} . i = diameter (S . i) );

for M being non empty Reflexive MetrStruct

for S being SetSequence of M

for b

( b

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

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

diameter S is real-valued ;

end;
let S be SetSequence of M;

coherence

diameter S is real-valued ;

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 )

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

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

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

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;

:: 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 );

for M being MetrStruct

for U being Subset of M holds

( U is open iff U in Family_open_set M );

definition
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 );

for M being MetrStruct

for A being Subset of M holds

( A is closed iff A ` is open );

registration

let M be MetrStruct ;

coherence

for b_{1} being Subset of M st b_{1} is empty holds

b_{1} is open

for b_{1} being Subset of M st b_{1} is empty holds

b_{1} is closed

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let M be non empty MetrStruct ;

existence

ex b_{1} being Subset of M st

( b_{1} is open & not b_{1} is empty )

ex b_{1} being Subset of M st

( b_{1} is closed & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

existence ex b

( b

proof 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 ) )

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;

:: 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 );

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 );

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;

ex b_{1} being SetSequence of T st b_{1} is open

ex b_{1} being SetSequence of T st b_{1} is closed

end;
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

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

proof end;

registration

let T be non empty TopSpace;

ex b_{1} being SetSequence of T st

( b_{1} is open & b_{1} is non-empty )

ex b_{1} being SetSequence of T st

( b_{1} is closed & b_{1} is non-empty )

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) open for Element of bool [:omega,(bool the carrier of T):];

existence ex b

( b

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

( b

proof 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 );

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 );

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;

ex b_{1} being SetSequence of M st

( b_{1} is non-empty & b_{1} is pointwise_bounded & b_{1} is open )

ex b_{1} being SetSequence of M st

( b_{1} is non-empty & b_{1} is pointwise_bounded & b_{1} is closed )

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 open for Element of bool [:omega,(bool the carrier of M):];

existence ex b

( b

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

( b

proof 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 ) )

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 )

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 ) ) )

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 )

( 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

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 ) )

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 } ) )

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 )

( 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 )

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

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

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 )

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 )

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 ;

end;
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 );

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 );

:: 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 ) );

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 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 <> {} )

( 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 <> {} )

( 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 } ) ) )

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;

::$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

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 )

( 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 )

( 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 )

( 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

scheme :: COMPL_SP:sch 1

Th39{ F_{1}() -> non empty set , P_{1}[ set , set ] } :

Th39{ F

ex A being Subset of F_{1}() st

( ( for x, y being Element of F_{1}() st x in A & y in A & x <> y holds

P_{1}[x,y] ) & ( for x being Element of F_{1}() ex y being Element of F_{1}() st

( y in A & P_{1}[x,y] ) ) )

provided( ( for x, y being Element of F

P

( y in A & P

A1:
for x, y being Element of F_{1}() holds

( P_{1}[x,y] iff P_{1}[y,x] )
and

A2: for x being Element of F_{1}() holds P_{1}[x,x]

( P

A2: for x being Element of F

proof end;

scheme :: COMPL_SP:sch 2

Th39{ F_{1}() -> non empty set , P_{1}[ set , set ] } :

Th39{ F

ex A being Subset of F_{1}() st

( ( for x, y being Element of F_{1}() st x in A & y in A & x <> y holds

P_{1}[x,y] ) & ( for x being Element of F_{1}() ex y being Element of F_{1}() st

( y in A & P_{1}[x,y] ) ) )

provided( ( for x, y being Element of F

P

( y in A & P

A1:
for x, y being Element of F_{1}() holds

( P_{1}[x,y] iff P_{1}[y,x] )
and

A2: for x being Element of F_{1}() holds P_{1}[x,x]

( P

A2: for x being Element of F

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) ) ) )

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 )

( 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

M is totally_bounded

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 )

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 )

( 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 )

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 ) )

( 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 ) ) ) )

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 ;

ex b_{1} 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_{1} . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies b_{1} . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) )

for b_{1}, b_{2} 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_{1} . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies b_{1} . (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_{2} . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies b_{2} . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) ) holds

b_{1} = b_{2}

end;
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 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)) ) );

ex b

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

proof end;

uniqueness for b

for x1, y1 being object

for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds

( ( x1 = y1 implies b

for x1, y1 being object

for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds

( ( x1 = y1 implies b

b

proof 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_{4} being Function of [:([:X,( the carrier of M \ {a}):] \/ {[X,a]}),([:X,( the carrier of M \ {a}):] \/ {[X,a]}):],REAL holds

( b_{4} = 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_{4} . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies b_{4} . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) );

for M being MetrStruct

for a being Point of M

for X being set

for b

( b

for x1, y1 being object

for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds

( ( x1 = y1 implies b

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 ) )

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 ;

MetrStruct(# ([:X,( the carrier of M \ {a}):] \/ {[X,a]}),(well_dist (a,X)) #) is strict MetrStruct ;

end;
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)) #);

MetrStruct(# ([:X,( the carrier of M \ {a}):] \/ {[X,a]}),(well_dist (a,X)) #) is strict MetrStruct ;

:: 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)) #);

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
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 ;

coherence

WellSpace (a,X) is Reflexive by Lm8;

end;
let a be Point of M;

let X be set ;

coherence

WellSpace (a,X) is Reflexive by Lm8;

registration

let M be symmetric MetrStruct ;

let a be Point of M;

let X be set ;

coherence

WellSpace (a,X) is symmetric by Lm8;

end;
let a be Point of M;

let X be set ;

coherence

WellSpace (a,X) is symmetric by Lm8;

registration

let M be Reflexive symmetric triangle MetrStruct ;

let a be Point of M;

let X be set ;

coherence

WellSpace (a,X) is triangle by Lm8;

end;
let a be Point of M;

let X be set ;

coherence

WellSpace (a,X) is triangle by Lm8;

registration

let M be MetrSpace;

let a be Point of M;

let X be set ;

coherence

WellSpace (a,X) is discerning by Lm8;

end;
let a be Point of M;

let X be set ;

coherence

WellSpace (a,X) is discerning by Lm8;

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

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] )

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

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 ) )

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 ) )

( 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;