:: Complete Spaces
:: by Karol P\c{a}k
::
:: Received October 12, 2007
:: Copyright (c) 2007 Association of Mizar Users
:: deftheorem Def1 defines bounded COMPL_SP:def 1 :
:: deftheorem Def2 defines diameter COMPL_SP:def 2 :
theorem Th1: :: COMPL_SP:1
theorem Th2: :: COMPL_SP:2
theorem :: COMPL_SP:3
theorem Th4: :: COMPL_SP:4
theorem Th5: :: COMPL_SP:5
:: deftheorem Def3 defines open COMPL_SP:def 3 :
:: deftheorem Def4 defines closed COMPL_SP:def 4 :
theorem Th6: :: COMPL_SP:6
:: deftheorem Def5 defines open COMPL_SP:def 5 :
:: deftheorem Def6 defines closed COMPL_SP:def 6 :
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 ) )
:: deftheorem Def7 defines open COMPL_SP:def 7 :
:: deftheorem Def8 defines closed COMPL_SP:def 8 :
theorem Th7: :: COMPL_SP:7
theorem Th8: :: COMPL_SP:8
theorem Th9: :: COMPL_SP:9
theorem Th10: :: COMPL_SP:10
theorem Th11: :: COMPL_SP:11
theorem Th12: :: COMPL_SP:12
theorem Th13: :: COMPL_SP:13
theorem :: COMPL_SP:14
theorem Th15: :: COMPL_SP:15
theorem Th16: :: COMPL_SP:16
theorem Th17: :: COMPL_SP:17
theorem Th18: :: COMPL_SP:18
theorem :: COMPL_SP:19
:: deftheorem Def9 defines countably_compact COMPL_SP:def 9 :
theorem Th20: :: COMPL_SP:20
theorem Th21: :: COMPL_SP:21
theorem Th22: :: COMPL_SP:22
theorem Th23: :: COMPL_SP:23
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
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
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 not A is finite holds
not Der A is empty
theorem Th24: :: COMPL_SP:24
theorem Th25: :: COMPL_SP:25
Lm5:
for T being non empty T_1 TopSpace st ( for A being Subset of T st not A is finite & A is countable holds
not Der A is empty ) holds
T is countably_compact
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
theorem Th26: :: COMPL_SP:26
theorem Th27: :: COMPL_SP:27
theorem Th28: :: COMPL_SP:28
theorem :: COMPL_SP:29
theorem Th30: :: COMPL_SP:30
theorem Th31: :: COMPL_SP:31
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
theorem Th32: :: COMPL_SP:32
theorem Th33: :: COMPL_SP:33
theorem Th34: :: COMPL_SP:34
theorem Th35: :: COMPL_SP:35
theorem Th36: :: COMPL_SP:36
theorem :: COMPL_SP:37
theorem Th38: :: COMPL_SP:38
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
set 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 set
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) ) )
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 set
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 set
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
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
set 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
:: deftheorem defines WellSpace COMPL_SP:def 11 :
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 ) )
theorem :: COMPL_SP:40
theorem Th41: :: COMPL_SP:41
theorem Th42: :: COMPL_SP:42
theorem Th43: :: COMPL_SP:43
theorem :: COMPL_SP:44