:: by Leszek Borys

::

:: Received July 23, 1992

:: Copyright (c) 1992-2019 Association of Mizar Users

theorem Th1: :: PCOMPS_2:1

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) )

for A being set st R well_orders A holds

( R |_2 A well_orders A & A = field (R |_2 A) )

proof end;

definition
end;

:: deftheorem defines PartUnion PCOMPS_2:def 1 :

for FX being set

for R being Relation

for B being Element of FX holds PartUnion (B,R) = union (R -Seg B);

for FX being set

for R being Relation

for B being Element of FX holds PartUnion (B,R) = union (R -Seg B);

definition

let FX be set ;

let R be Relation;

ex b_{1} being set st

for A being set holds

( A in b_{1} iff ex B being Element of FX st

( B in FX & A = B \ (PartUnion (B,R)) ) )

for b_{1}, b_{2} being set st ( for A being set holds

( A in b_{1} iff ex B being Element of FX st

( B in FX & A = B \ (PartUnion (B,R)) ) ) ) & ( for A being set holds

( A in b_{2} iff ex B being Element of FX st

( B in FX & A = B \ (PartUnion (B,R)) ) ) ) holds

b_{1} = b_{2}

end;
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 for A being set holds

( A in it iff ex B being Element of FX st

( B in FX & A = B \ (PartUnion (B,R)) ) );

ex b

for A being set holds

( A in b

( B in FX & A = B \ (PartUnion (B,R)) ) )

proof end;

uniqueness for b

( A in b

( B in FX & A = B \ (PartUnion (B,R)) ) ) ) & ( for A being set holds

( A in b

( B in FX & A = B \ (PartUnion (B,R)) ) ) ) holds

b

proof end;

:: deftheorem defines DisjointFam PCOMPS_2:def 2 :

for FX being set

for R being Relation

for b_{3} being set holds

( b_{3} = DisjointFam (FX,R) iff for A being set holds

( A in b_{3} iff ex B being Element of FX st

( B in FX & A = B \ (PartUnion (B,R)) ) ) );

for FX being set

for R being Relation

for b

( b

( A in b

( B in FX & A = B \ (PartUnion (B,R)) ) ) );

definition

let X be set ;

let n be Element of NAT ;

let f be sequence of (bool X);

coherence

union (f .: ((Seg n) \ {n})) is set ;

end;
let n be Element of NAT ;

let f be sequence of (bool X);

coherence

union (f .: ((Seg n) \ {n})) is set ;

:: deftheorem defines PartUnionNat PCOMPS_2:def 3 :

for X being set

for n being Element of NAT

for f being sequence of (bool X) holds PartUnionNat (n,f) = union (f .: ((Seg n) \ {n}));

for X being set

for n being Element of NAT

for f being sequence of (bool X) holds PartUnionNat (n,f) = union (f .: ((Seg n) \ {n}));

theorem Th2: :: PCOMPS_2:2

for PT being non empty TopSpace st PT is regular holds

for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds

ex HX being Subset-Family of PT st

( HX is open & HX is 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 ) ) )

for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds

ex HX being Subset-Family of PT st

( HX is open & HX is 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:3

for PT being non empty TopSpace

for FX being Subset-Family of PT st PT is T_2 & PT is paracompact & FX is Cover of PT & FX is open holds

ex GX being Subset-Family of PT st

( GX is open & GX is Cover of PT & clf GX is_finer_than FX & GX is locally_finite )

for FX being Subset-Family of PT st PT is T_2 & PT is paracompact & FX is Cover of PT & FX is open holds

ex GX being Subset-Family of PT st

( GX is open & GX is Cover of PT & clf GX is_finer_than FX & GX is locally_finite )

proof end;

theorem Th4: :: PCOMPS_2:4

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

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:5

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 Th4;

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 Th4;

scheme :: PCOMPS_2:sch 2

XXX1{ F_{1}() -> non empty set , F_{2}() -> Subset-Family of F_{1}(), F_{3}( object , object ) -> Subset of F_{1}(), P_{1}[ object ], P_{2}[ object , object , object , object ] } :

XXX1{ F

ex f being sequence of (bool (bool F_{1}())) st

( f . 0 = F_{2}() & ( for n being Nat holds f . (n + 1) = { (union { F_{3}(c,n) where c is Element of F_{1}() : for fq being Subset-Family of F_{1}()

for q being Nat st q <= n & fq = f . q holds

P_{2}[c,V,n,fq] } ) where V is Subset of F_{1}() : P_{1}[V] } ) )

( f . 0 = F

for q being Nat st q <= n & fq = f . q holds

P

proof end;

reconsider jd = 1 / 2 as Real ;

scheme :: PCOMPS_2:sch 3

XXX{ F_{1}() -> non empty set , F_{2}() -> Subset-Family of F_{1}(), F_{3}( object , object ) -> Subset of F_{1}(), P_{1}[ object ], P_{2}[ object , object , object ] } :

XXX{ F

ex f being sequence of (bool (bool F_{1}())) st

( f . 0 = F_{2}() & ( for n being Nat holds f . (n + 1) = { (union { F_{3}(c,n) where c is Element of F_{1}() : ( P_{2}[c,V,n] & not c in union { (union (f . q)) where q is Nat : q <= n } ) } ) where V is Subset of F_{1}() : P_{1}[V] } ) )

( f . 0 = F

proof end;

theorem Th6: :: PCOMPS_2:6

for PT being non empty TopSpace st PT is metrizable holds

for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds

ex GX being Subset-Family of PT st

( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite )

for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds

ex GX being Subset-Family of PT st

( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite )

proof end;