:: PCOMPS_2 semantic presentation

theorem :: PCOMPS_2:1

canceled;

theorem :: PCOMPS_2:2

canceled;

theorem Th3: :: PCOMPS_2:3

for r, u being real number st r > 0 & u > 0 holds
ex k being Nat st u / (2 |^ k) <= r

proof end;

theorem Th4: :: PCOMPS_2:4

for r being real number
for k, n being Nat st k >= n & r >= 1 holds
r |^ k >= r |^ n

proof end;

theorem Th5: :: PCOMPS_2:5

for R being Relation
for A being set st R well_orders A holds
( R |_2 A well_orders A & A = field (R |_2 A) )

proof end;

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

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

provided

A1: F₂() well_orders F₁() and
A2: ex X being set st
( X in F₁() & P₁[X] )

proof end;

definition

let FX be set ;
let R be Relation;
let B be Element of FX;
func PartUnion B,R -> set equals :: PCOMPS_2:def 1
union (R -Seg B);
coherence ;

end;

:: deftheorem defines PartUnion PCOMPS_2:def 1 :

definition

let FX be set ;
let R be Relation;
func DisjointFam FX,R -> set means :: PCOMPS_2:def 2
for A being set holds
( A in it iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion B,R) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines DisjointFam PCOMPS_2:def 2 :

definition

let X be set ;
let n be Nat;
let f be Function of NAT , bool X;
func PartUnionNat n,f -> set equals :: PCOMPS_2:def 3
union (f .: ((Seg n) \ {n}));
coherence ;

end;

:: deftheorem defines PartUnionNat PCOMPS_2:def 3 :

theorem Th6: :: PCOMPS_2:6

for PT being non empty TopSpace st PT is_T3 holds
for FX being Subset-Family of PT st FX is_a_cover_of PT & FX is open holds
ex HX being Subset-Family of PT st
( HX is open & HX is_a_cover_of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) )

proof end;

theorem :: PCOMPS_2:7

for PT being non empty TopSpace
for FX being Subset-Family of PT st PT is_T2 & PT is paracompact & FX is_a_cover_of PT & FX is open holds
ex GX being Subset-Family of PT st
( GX is open & GX is_a_cover_of PT & clf GX is_finer_than FX & GX is locally_finite )

proof end;

theorem Th8: :: PCOMPS_2:8

for PT being non empty TopSpace
for PM being MetrSpace
for f being Function of [:the carrier of PT,the carrier of PT:], REAL st f is_metric_of the carrier of PT & PM = SpaceMetr the carrier of PT,f holds
the carrier of PM = the carrier of PT

proof end;

theorem :: PCOMPS_2:9

canceled;

theorem :: PCOMPS_2:10

canceled;

theorem :: PCOMPS_2:11

for PT being non empty TopSpace
for PM being MetrSpace
for FX being Subset-Family of PT
for f being Function of [:the carrier of PT,the carrier of PT:], REAL st f is_metric_of the carrier of PT & PM = SpaceMetr the carrier of PT,f holds
( FX is Subset-Family of PT iff FX is Subset-Family of PM ) by Th8;

definition

let PM be non empty set ;
let g be Function of NAT ,(bool (bool PM)) * ;
let n be Nat;
:: original: .
redefine func g . n -> FinSequence of bool (bool PM);
coherence

proof end;

end;

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

ex f being Function of NAT , bool (bool F₁()) st
( f . 0 = F₂() & ( for n being Nat holds f . (n + 1) = { (union { F₃(c,n) where c is Element of F₁() : for fq being Subset-Family of F₁()
for q being Nat st q <= n & fq = f . q holds
P₂[c,V,n,fq] } ) where V is Subset of F₁() : P₁[V] } ) )

proof end;

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

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

proof end;

theorem Th12: :: PCOMPS_2:12

for PT being non empty TopSpace st PT is metrizable holds
for FX being Subset-Family of PT st FX is_a_cover_of PT & FX is open holds
ex GX being Subset-Family of PT st
( GX is open & GX is_a_cover_of PT & GX is_finer_than FX & GX is locally_finite )

proof end;

theorem :: PCOMPS_2:13

for PT being non empty TopSpace st PT is metrizable holds
PT is paracompact

proof end;