:: PCOMPS_2 semantic presentation

theorem Th1: :: PCOMPS_2:1

canceled;

theorem Th2: :: PCOMPS_2:2

canceled;

theorem Th3: :: PCOMPS_2:3

for b₁, b₂ being real number st b₁ > 0 & b₂ > 0 holds
ex b₃ being Nat st b₂ / (2 |^ b₃) <= b₁

proof end;

theorem Th4: :: PCOMPS_2:4

for b₁ being real number
for b₂, b₃ being Nat st b₂ >= b₃ & b₁ >= 1 holds
b₁ |^ b₂ >= b₁ |^ b₃

proof end;

theorem Th5: :: PCOMPS_2:5

for b₁ being Relation
for b₂ being set st b₁ well_orders b₂ holds
( b₁ |_2 b₂ well_orders b₂ & b₂ = field (b₁ |_2 b₂) )

proof end;

scheme :: PCOMPS_2:sch 1
s1{ F₁() -> set , F₂() -> Relation, P₁[ set ] } :

ex b₁ being set st
( b₁ in F₁() & P₁[b₁] & ( for b₂ being set st b₂ in F₁() & P₁[b₂] holds
[b₁,b₂] in F₂() ) )

provided

E4: F₂() well_orders F₁() and
E5: ex b₁ being set st
( b₁ in F₁() & P₁[b₁] )

proof end;

definition

let c₁ be set ;
let c₂ be Relation;
let c₃ be Element of c₁;
func PartUnion c₃,c₂ -> set equals :: PCOMPS_2:def 1
union (a₂ -Seg a₃);
coherence ;

end;

:: deftheorem Def1 defines PartUnion PCOMPS_2:def 1 :

definition

let c₁ be set ;
let c₂ be Relation;
func DisjointFam c₁,c₂ -> set means :: PCOMPS_2:def 2
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being Element of a₁ st
( b₂ in a₁ & b₁ = b₂ \ (PartUnion b₂,a₂) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines DisjointFam PCOMPS_2:def 2 :

definition

let c₁ be set ;
let c₂ be Nat;
let c₃ be Function of NAT , bool c₁;
func PartUnionNat c₂,c₃ -> set equals :: PCOMPS_2:def 3
union (a₃ .: ((Seg a₂) \ {a₂}));
coherence ;

end;

:: deftheorem Def3 defines PartUnionNat PCOMPS_2:def 3 :

theorem Th6: :: PCOMPS_2:6

for b₁ being non empty TopSpace st b₁ is_T3 holds
for b₂ being Subset-Family of b₁ st b₂ is_a_cover_of b₁ & b₂ is open holds
ex b₃ being Subset-Family of b₁ st
( b₃ is open & b₃ is_a_cover_of b₁ & ( for b₄ being Subset of b₁ st b₄ in b₃ holds
ex b₅ being Subset of b₁ st
( b₅ in b₂ & Cl b₄ c= b₅ ) ) )

proof end;

theorem Th7: :: PCOMPS_2:7

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₁ is_T2 & b₁ is paracompact & b₂ is_a_cover_of b₁ & b₂ is open holds
ex b₃ being Subset-Family of b₁ st
( b₃ is open & b₃ is_a_cover_of b₁ & clf b₃ is_finer_than b₂ & b₃ is locally_finite )

proof end;

theorem Th8: :: PCOMPS_2:8

for b₁ being non empty TopSpace
for b₂ being MetrSpace
for b₃ being Function of [:the carrier of b₁,the carrier of b₁:], REAL st b₃ is_metric_of the carrier of b₁ & b₂ = SpaceMetr the carrier of b₁,b₃ holds
the carrier of b₂ = the carrier of b₁

proof end;

theorem Th9: :: PCOMPS_2:9

canceled;

theorem Th10: :: PCOMPS_2:10

canceled;

theorem Th11: :: PCOMPS_2:11

for b₁ being non empty TopSpace
for b₂ being MetrSpace
for b₃ being Subset-Family of b₁
for b₄ being Function of [:the carrier of b₁,the carrier of b₁:], REAL st b₄ is_metric_of the carrier of b₁ & b₂ = SpaceMetr the carrier of b₁,b₄ holds
( b₃ is Subset-Family of b₁ iff b₃ is Subset-Family of b₂ ) by Th8;

definition

let c₁ be non empty set ;
let c₂ be Function of NAT ,(bool (bool c₁)) * ;
let c₃ be Nat;
redefine func . as c₂ . c₃ -> FinSequence of bool (bool a₁);
coherence

proof end;

end;

scheme :: PCOMPS_2:sch 2
s2{ F₁() -> non empty set , F₂() -> Subset-Family of F₁(), F₃( set , set ) -> Subset of F₁(), P₁[ set ], P₂[ set , set , set , set ] } :

ex b₁ being Function of NAT , bool (bool F₁()) st
( b₁ . 0 = F₂() & ( for b₂ being Nat holds b₁ . (b₂ + 1) = { (union { F₃(b₄,b₂) where B is Element of F₁() : for b₁ being Subset-Family of F₁()
for b₂ being Nat st b₆ <= b₂ & b₅ = b₁ . b₆ holds
P₂[b₄,b₃,b₂,b₅] } ) where B is Subset of F₁() : P₁[b₃] } ) )

proof end;

scheme :: PCOMPS_2:sch 3
s3{ F₁() -> non empty set , F₂() -> Subset-Family of F₁(), F₃( set , set ) -> Subset of F₁(), P₁[ set ], P₂[ set , set , set ] } :

ex b₁ being Function of NAT , bool (bool F₁()) st
( b₁ . 0 = F₂() & ( for b₂ being Nat holds b₁ . (b₂ + 1) = { (union { F₃(b₄,b₂) where B is Element of F₁() : ( P₂[b₄,b₃,b₂] & not b₄ in union { (union (b₁ . b₅)) where B is Nat : b₅ <= b₂ } ) } ) where B is Subset of F₁() : P₁[b₃] } ) )

proof end;

theorem Th12: :: PCOMPS_2:12

for b₁ being non empty TopSpace st b₁ is metrizable holds
for b₂ being Subset-Family of b₁ st b₂ is_a_cover_of b₁ & b₂ is open holds
ex b₃ being Subset-Family of b₁ st
( b₃ is open & b₃ is_a_cover_of b₁ & b₃ is_finer_than b₂ & b₃ is locally_finite )

proof end;

theorem Th13: :: PCOMPS_2:13

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

proof end;