:: PCOMPS_1 semantic presentation

theorem Th1: :: PCOMPS_1:1

for b₁ being MetrStruct
for b₂ being Element of b₁
for b₃, b₄ being real number st b₃ <= b₄ holds
Ball b₂,b₃ c= Ball b₂,b₄

proof end;

theorem Th2: :: PCOMPS_1:2

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( Cl b₂ <> {} iff b₂ <> {} )

proof end;

theorem Th3: :: PCOMPS_1:3

canceled;

theorem Th4: :: PCOMPS_1:4

canceled;

theorem Th5: :: PCOMPS_1:5

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is_a_cover_of b₁ holds
for b₃ being Point of b₁ ex b₄ being Subset of b₁ st
( b₃ in b₄ & b₄ in b₂ )

proof end;

definition

let c₁ be set ;
redefine func bool as bool c₁ -> Subset-Family of a₁;
coherence by ZFMISC_1:def 1;

end;

definition

let c₁ be set ;
func 1TopSp c₁ -> TopStruct equals :: PCOMPS_1:def 1
TopStruct(# a₁,(bool a₁) #);
coherence ;

end;

:: deftheorem Def1 defines 1TopSp PCOMPS_1:def 1 :

registration

let c₁ be set ;
cluster 1TopSp a₁ -> strict TopSpace-like ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
cluster 1TopSp a₁ -> non empty strict TopSpace-like ;
coherence ;

end;

theorem Th6: :: PCOMPS_1:6

canceled;

theorem Th7: :: PCOMPS_1:7

for b₁ being set holds the topology of (1TopSp b₁) = bool b₁ ;

theorem Th8: :: PCOMPS_1:8

for b₁ being set holds the carrier of (1TopSp b₁) = b₁ ;

theorem Th9: :: PCOMPS_1:9

for b₁ being set holds 1TopSp {b₁} is compact

proof end;

theorem Th10: :: PCOMPS_1:10

for b₁ being non empty TopSpace
for b₂ being Point of b₁ st b₁ is_T2 holds
{b₂} is closed

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset-Family of c₁;
attr a₂ is locally_finite means :Def2: :: PCOMPS_1:def 2
for b₁ being Point of a₁ ex b₂ being Subset of a₁ st
( b₁ in b₂ & b₂ is open & { b₃ where B is Subset of a₁ : ( b₃ in a₂ & b₃ meets b₂ ) } is finite );

end;

:: deftheorem Def2 defines locally_finite PCOMPS_1:def 2 :

theorem Th11: :: PCOMPS_1:11

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁
for b₃ being Subset of b₁ holds { b₄ where B is Subset of b₁ : ( b₄ in b₂ & b₄ meets b₃ ) } c= b₂

proof end;

theorem Th12: :: PCOMPS_1:12

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ c= b₃ & b₃ is locally_finite holds
b₂ is locally_finite

proof end;

theorem Th13: :: PCOMPS_1:13

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is finite holds
b₂ is locally_finite

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset-Family of c₁;
func clf c₂ -> Subset-Family of a₁ means :Def3: :: PCOMPS_1:def 3
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff ex b₂ being Subset of a₁ st
( b₁ = Cl b₂ & b₂ in a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines clf PCOMPS_1:def 3 :

theorem Th14: :: PCOMPS_1:14

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ holds clf b₂ is closed

proof end;

theorem Th15: :: PCOMPS_1:15

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ st b₂ = {} holds
clf b₂ = {}

proof end;

theorem Th16: :: PCOMPS_1:16

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Subset-Family of b₁ st b₃ = {b₂} holds
clf b₃ = {(Cl b₂)}

proof end;

theorem Th17: :: PCOMPS_1:17

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ st b₂ c= b₃ holds
clf b₂ c= clf b₃

proof end;

theorem Th18: :: PCOMPS_1:18

for b₁ being non empty TopSpace
for b₂, b₃ being Subset-Family of b₁ holds clf (b₂ \/ b₃) = (clf b₂) \/ (clf b₃)

proof end;

theorem Th19: :: PCOMPS_1:19

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is finite holds
Cl (union b₂) = union (clf b₂)

proof end;

theorem Th20: :: PCOMPS_1:20

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ holds b₂ is_finer_than clf b₂

proof end;

scheme :: PCOMPS_1:sch 1
s1{ F₁() -> TopSpace, F₂() -> Subset-Family of F₁(), F₃() -> Subset-Family of F₁(), F₄( set ) -> Subset of F₁() } :

ex b₁ being Function of F₂(),F₃() st
for b₂ being Subset of F₁() st b₂ in F₂() holds
b₁ . b₂ = F₄(b₂)

provided

E17: for b₁ being Subset of F₁() st b₁ in F₂() holds
F₄(b₁) in F₃()

proof end;

theorem Th21: :: PCOMPS_1:21

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is locally_finite holds
clf b₂ is locally_finite

proof end;

theorem Th22: :: PCOMPS_1:22

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ holds union b₂ c= union (clf b₂)

proof end;

theorem Th23: :: PCOMPS_1:23

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is locally_finite holds
Cl (union b₂) = union (clf b₂)

proof end;

theorem Th24: :: PCOMPS_1:24

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is locally_finite & b₂ is closed holds
union b₂ is closed

proof end;

definition

let c₁ be TopStruct ;
attr a₁ is paracompact means :Def4: :: PCOMPS_1:def 4
for b₁ being Subset-Family of a₁ st b₁ is_a_cover_of a₁ & b₁ is open holds
ex b₂ being Subset-Family of a₁ st
( b₂ is open & b₂ is_a_cover_of a₁ & b₂ is_finer_than b₁ & b₂ is locally_finite );

end;

:: deftheorem Def4 defines paracompact PCOMPS_1:def 4 :

registration

cluster non empty paracompact TopStruct ;
existence

proof end;

end;

theorem Th25: :: PCOMPS_1:25

for b₁ being non empty TopSpace st b₁ is compact holds
b₁ is paracompact

proof end;

theorem Th26: :: PCOMPS_1:26

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₁ is paracompact & b₂ is closed & b₃ is closed & b₂ misses b₃ & ( for b₄ being Point of b₁ st b₄ in b₃ holds
ex b₅, b₆ being Subset of b₁ st
( b₅ is open & b₆ is open & b₂ c= b₅ & b₄ in b₆ & b₅ misses b₆ ) ) holds
ex b₄, b₅ being Subset of b₁ st
( b₄ is open & b₅ is open & b₂ c= b₄ & b₃ c= b₅ & b₄ misses b₅ )

proof end;

theorem Th27: :: PCOMPS_1:27

for b₁ being non empty TopSpace st b₁ is_T2 & b₁ is paracompact holds
b₁ is_T3

proof end;

theorem Th28: :: PCOMPS_1:28

for b₁ being non empty TopSpace st b₁ is_T2 & b₁ is paracompact holds
b₁ is_T4

proof end;

definition

let c₁ be MetrStruct ;
func Family_open_set c₁ -> Subset-Family of a₁ means :Def5: :: PCOMPS_1:def 5
for b₁ being Subset of a₁ holds
( b₁ in a₂ iff for b₂ being Element of a₁ st b₂ in b₁ holds
ex b₃ being Real st
( b₃ > 0 & Ball b₂,b₃ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Family_open_set PCOMPS_1:def 5 :

theorem Th29: :: PCOMPS_1:29

for b₁ being MetrStruct
for b₂ being Element of b₁ ex b₃ being Real st
( b₃ > 0 & Ball b₂,b₃ c= the carrier of b₁ )

proof end;

theorem Th30: :: PCOMPS_1:30

for b₁ being MetrStruct
for b₂, b₃ being Element of b₁
for b₄ being real number st b₁ is triangle & b₂ in Ball b₃,b₄ holds
ex b₅ being Real st
( b₅ > 0 & Ball b₂,b₅ c= Ball b₃,b₄ )

proof end;

theorem Th31: :: PCOMPS_1:31

for b₁ being MetrStruct
for b₂, b₃ being Real
for b₄, b₅, b₆ being Element of b₁ st b₁ is triangle & b₄ in (Ball b₅,b₂) /\ (Ball b₆,b₃) holds
ex b₇ being Real st
( Ball b₄,b₇ c= Ball b₅,b₂ & Ball b₄,b₇ c= Ball b₆,b₃ )

proof end;

theorem Th32: :: PCOMPS_1:32

canceled;

theorem Th33: :: PCOMPS_1:33

for b₁ being MetrStruct
for b₂ being Element of b₁
for b₃ being real number st b₁ is triangle holds
Ball b₂,b₃ in Family_open_set b₁

proof end;

theorem Th34: :: PCOMPS_1:34

for b₁ being MetrStruct holds the carrier of b₁ in Family_open_set b₁

proof end;

theorem Th35: :: PCOMPS_1:35

for b₁ being MetrStruct
for b₂, b₃ being Subset of b₁ st b₂ in Family_open_set b₁ & b₃ in Family_open_set b₁ holds
b₂ /\ b₃ in Family_open_set b₁

proof end;

theorem Th36: :: PCOMPS_1:36

for b₁ being MetrStruct
for b₂ being Subset-Family of b₁ st b₂ c= Family_open_set b₁ holds
union b₂ in Family_open_set b₁

proof end;

theorem Th37: :: PCOMPS_1:37

for b₁ being MetrStruct holds TopStruct(# the carrier of b₁,(Family_open_set b₁) #) is TopSpace

proof end;

definition

let c₁ be MetrStruct ;
func TopSpaceMetr c₁ -> TopStruct equals :: PCOMPS_1:def 6
TopStruct(# the carrier of a₁,(Family_open_set a₁) #);
coherence ;

end;

:: deftheorem Def6 defines TopSpaceMetr PCOMPS_1:def 6 :

registration

let c₁ be MetrStruct ;
cluster TopSpaceMetr a₁ -> strict TopSpace-like ;
coherence by Th37;

end;

registration

let c₁ be non empty MetrStruct ;
cluster TopSpaceMetr a₁ -> non empty strict TopSpace-like ;
coherence ;

end;

theorem Th38: :: PCOMPS_1:38

for b₁ being non empty MetrSpace holds TopSpaceMetr b₁ is_T2

proof end;

registration

cluster non empty strict being_T2 TopStruct ;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Function of [:c₁,c₁:], REAL ;
pred c₂ is_metric_of c₁ means :Def7: :: PCOMPS_1:def 7
for b₁, b₂, b₃ being Element of a₁ holds
( ( a₂ . b₁,b₂ = 0 implies b₁ = b₂ ) & ( b₁ = b₂ implies a₂ . b₁,b₂ = 0 ) & a₂ . b₁,b₂ = a₂ . b₂,b₁ & a₂ . b₁,b₃ <= (a₂ . b₁,b₂) + (a₂ . b₂,b₃) );

end;

:: deftheorem Def7 defines is_metric_of PCOMPS_1:def 7 :

theorem Th39: :: PCOMPS_1:39

for b₁ being set
for b₂ being Function of [:b₁,b₁:], REAL holds
( b₂ is_metric_of b₁ iff MetrStruct(# b₁,b₂ #) is MetrSpace )

proof end;

definition

let c₁ be non empty set ;
let c₂ be Function of [:c₁,c₁:], REAL ;
assume E33: c₂ is_metric_of c₁ ;
func SpaceMetr c₁,c₂ -> non empty strict MetrSpace equals :Def8: :: PCOMPS_1:def 8
MetrStruct(# a₁,a₂ #);
coherence by E33, Th39;

end;

:: deftheorem Def8 defines SpaceMetr PCOMPS_1:def 8 :

definition

let c₁ be non empty TopStruct ;
attr a₁ is metrizable means :: PCOMPS_1:def 9
ex b₁ being Function of [:the carrier of a₁,the carrier of a₁:], REAL st
( b₁ is_metric_of the carrier of a₁ & Family_open_set (SpaceMetr the carrier of a₁,b₁) = the topology of a₁ );

end;

:: deftheorem Def9 defines metrizable PCOMPS_1:def 9 :

registration

cluster non empty strict metrizable TopStruct ;
existence

proof end;

end;