begin
:: deftheorem Def1 defines bounded COMPL_SP:def 1 :
:: deftheorem Def2 defines diameter COMPL_SP:def 2 :
theorem Th1:
theorem Th2:
theorem
theorem Th4:
theorem Th5:
:: deftheorem Def3 defines open COMPL_SP:def 3 :
:: deftheorem Def4 defines closed COMPL_SP:def 4 :
theorem Th6:
:: 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:
theorem Th8:
begin
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
begin
:: deftheorem Def9 defines countably_compact COMPL_SP:def 9 :
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
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:
theorem Th25:
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:
theorem Th27:
theorem Th28:
theorem
scheme
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]
theorem Th30:
theorem Th31:
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:
theorem Th33:
theorem Th34:
begin
theorem Th35:
theorem Th36:
theorem
begin
theorem Th38:
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:
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
:: 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
theorem Th41:
theorem Th42:
theorem Th43:
theorem