:: by Roland Coghetto

::

:: Received March 31, 2014

:: Copyright (c) 2014-2018 Association of Mizar Users

registration

let X be set ;

let S be Subset-Family of X;

let S1, S2 be finite Subset of S;

coherence

INTERSECTION (S1,S2) is finite

end;
let S be Subset-Family of X;

let S1, S2 be finite Subset of S;

coherence

INTERSECTION (S1,S2) is finite

proof end;

theorem ThmVAL1: :: SRINGS_1:2

for X being set

for S being Subset-Family of X

for A being Element of S holds { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } = union ((PARTITIONS A) /\ (Fin S))

for S being Subset-Family of X

for A being Element of S holds { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } = union ((PARTITIONS A) /\ (Fin S))

proof end;

A4bis: PARTITIONS {} = {{}}

proof end;

registration

let X be set ;

let S be Subset-Family of X;

coherence

union ((PARTITIONS {}) /\ (Fin S)) is empty

end;
let S be Subset-Family of X;

coherence

union ((PARTITIONS {}) /\ (Fin S)) is empty

proof end;

Lem3: for X being set

for S being Subset-Family of X st ( for A, B being Element of S st not A \ B is empty holds

ex P being finite Subset of S st P is a_partition of A \ B ) holds

for A, B being Element of S ex P being finite Subset of S st P is a_partition of A \ B

proof end;

Lem4: for X being set holds

( ( for A, B being Element of cobool X st not A /\ B is empty holds

ex P being finite Subset of (cobool X) st P is a_partition of A /\ B ) & ( for A, B being Element of cobool X st B c= A holds

ex P being finite Subset of (cobool X) st P is a_partition of A \ B ) & ( for A, B being Element of cobool X st not A \ B is empty holds

ex P being finite Subset of (cobool X) st P is a_partition of A \ B ) & {X} is countable Subset of (cobool X) & union {X} = X )

proof end;

Lem5: for X being set

for S being Subset-Family of X

for A, B being Element of S

for p being finite Subset of S st B <> {} & B c= A & p is a_partition of A \ B holds

{B} \/ p is a_partition of A

proof end;

Lem6: for X being set

for S being non empty Subset-Family of X st ( for A, B being Element of S ex P being finite Subset of S st P is a_partition of A /\ B ) & ( for C, D being Element of S st D c= C holds

ex P being finite Subset of S st P is a_partition of C \ D ) holds

for A being Element of S

for Q being finite Subset of S st not A is empty & union Q c= A & Q is a_partition of union Q holds

ex R being finite Subset of S st

( union R misses union Q & Q \/ R is a_partition of A )

proof end;

definition

let X be set ;

let S be Subset-Family of X;

end;
let S be Subset-Family of X;

attr S is cap-finite-partition-closed means :Defcap: :: SRINGS_1:def 1

for S1, S2 being Element of S st not S1 /\ S2 is empty holds

ex x being finite Subset of S st x is a_partition of S1 /\ S2;

for S1, S2 being Element of S st not S1 /\ S2 is empty holds

ex x being finite Subset of S st x is a_partition of S1 /\ S2;

:: deftheorem Defcap defines cap-finite-partition-closed SRINGS_1:def 1 :

for X being set

for S being Subset-Family of X holds

( S is cap-finite-partition-closed iff for S1, S2 being Element of S st not S1 /\ S2 is empty holds

ex x being finite Subset of S st x is a_partition of S1 /\ S2 );

for X being set

for S being Subset-Family of X holds

( S is cap-finite-partition-closed iff for S1, S2 being Element of S st not S1 /\ S2 is empty holds

ex x being finite Subset of S st x is a_partition of S1 /\ S2 );

registration

let X be set ;

existence

ex b_{1} being Subset-Family of X st b_{1} is cap-finite-partition-closed

end;
existence

ex b

proof end;

registration

let X be set ;

coherence

for b_{1} being Subset-Family of X st b_{1} is cap-closed holds

b_{1} is cap-finite-partition-closed

end;
coherence

for b

b

proof end;

Lem7: for X being set

for S being cap-finite-partition-closed Subset-Family of X

for S1, S2 being Element of S ex P being finite Subset of S st P is a_partition of S1 /\ S2

proof end;

Th1: for X being set

for S being cap-finite-partition-closed Subset-Family of X

for P1, P2 being finite Subset of S

for y being non empty set st y in INTERSECTION (P1,P2) holds

ex P being finite Subset of S st P is a_partition of y

proof end;

theorem ThmJ1: :: SRINGS_1:4

for X being set

for A being non empty set

for S being cap-finite-partition-closed Subset-Family of X

for P1, P2 being a_partition of A st P1 is finite Subset of S & P2 is finite Subset of S holds

ex P being a_partition of A st

( P is finite Subset of S & P '<' P1 '/\' P2 )

for A being non empty set

for S being cap-finite-partition-closed Subset-Family of X

for P1, P2 being a_partition of A st P1 is finite Subset of S & P2 is finite Subset of S holds

ex P being a_partition of A st

( P is finite Subset of S & P '<' P1 '/\' P2 )

proof end;

theorem V: :: SRINGS_1:5

for X being set

for S being cap-finite-partition-closed Subset-Family of X

for A, B being finite Subset of S st A is mutually-disjoint & B is mutually-disjoint holds

ex P being finite Subset of S st P is a_partition of (union A) /\ (union B)

for S being cap-finite-partition-closed Subset-Family of X

for A, B being finite Subset of S st A is mutually-disjoint & B is mutually-disjoint holds

ex P being finite Subset of S st P is a_partition of (union A) /\ (union B)

proof end;

Lem8: for X being set

for S being cap-finite-partition-closed Subset-Family of X

for SM being FinSequence of S ex P being finite Subset of S st P is a_partition of meet (rng SM)

proof end;

theorem :: SRINGS_1:6

for X being set

for S being cap-finite-partition-closed Subset-Family of X

for SM being finite Subset of S ex P being finite Subset of S st P is a_partition of meet SM

for S being cap-finite-partition-closed Subset-Family of X

for SM being finite Subset of S ex P being finite Subset of S st P is a_partition of meet SM

proof end;

theorem Thm86: :: SRINGS_1:7

for X being set

for S being cap-finite-partition-closed Subset-Family of X holds { (union x) where x is finite Subset of S : x is mutually-disjoint } is cap-closed

for S being cap-finite-partition-closed Subset-Family of X holds { (union x) where x is finite Subset of S : x is mutually-disjoint } is cap-closed

proof end;

definition

let X be set ;

let S be Subset-Family of X;

end;
let S be Subset-Family of X;

attr S is diff-finite-partition-closed means :Defdiff: :: SRINGS_1:def 2

for S1, S2 being Element of S st not S1 \ S2 is empty holds

ex x being finite Subset of S st x is a_partition of S1 \ S2;

for S1, S2 being Element of S st not S1 \ S2 is empty holds

ex x being finite Subset of S st x is a_partition of S1 \ S2;

:: deftheorem Defdiff defines diff-finite-partition-closed SRINGS_1:def 2 :

for X being set

for S being Subset-Family of X holds

( S is diff-finite-partition-closed iff for S1, S2 being Element of S st not S1 \ S2 is empty holds

ex x being finite Subset of S st x is a_partition of S1 \ S2 );

for X being set

for S being Subset-Family of X holds

( S is diff-finite-partition-closed iff for S1, S2 being Element of S st not S1 \ S2 is empty holds

ex x being finite Subset of S st x is a_partition of S1 \ S2 );

registration

let X be set ;

existence

ex b_{1} being Subset-Family of X st b_{1} is diff-finite-partition-closed

end;
existence

ex b

proof end;

registration

let X be set ;

coherence

for b_{1} being Subset-Family of X st b_{1} is diff-closed holds

b_{1} is diff-finite-partition-closed

end;
coherence

for b

b

proof end;

theorem Thm1: :: SRINGS_1:8

for X being set

for S being diff-finite-partition-closed Subset-Family of X

for S1 being Element of S

for T being finite Subset of S ex P being finite Subset of S st P is a_partition of S1 \ (union T)

for S being diff-finite-partition-closed Subset-Family of X

for S1 being Element of S

for T being finite Subset of S ex P being finite Subset of S st P is a_partition of S1 \ (union T)

proof end;

definition

let X be set ;

let S be Subset-Family of X;

end;
let S be Subset-Family of X;

attr S is diff-c=-finite-partition-closed means :Defdiff2: :: SRINGS_1:def 3

for S1, S2 being Element of S st S2 c= S1 holds

ex x being finite Subset of S st x is a_partition of S1 \ S2;

for S1, S2 being Element of S st S2 c= S1 holds

ex x being finite Subset of S st x is a_partition of S1 \ S2;

:: deftheorem Defdiff2 defines diff-c=-finite-partition-closed SRINGS_1:def 3 :

for X being set

for S being Subset-Family of X holds

( S is diff-c=-finite-partition-closed iff for S1, S2 being Element of S st S2 c= S1 holds

ex x being finite Subset of S st x is a_partition of S1 \ S2 );

for X being set

for S being Subset-Family of X holds

( S is diff-c=-finite-partition-closed iff for S1, S2 being Element of S st S2 c= S1 holds

ex x being finite Subset of S st x is a_partition of S1 \ S2 );

theorem Thm2: :: SRINGS_1:9

for X being set

for S being Subset-Family of X st S is diff-finite-partition-closed holds

S is diff-c=-finite-partition-closed

for S being Subset-Family of X st S is diff-finite-partition-closed holds

S is diff-c=-finite-partition-closed

proof end;

registration

let X be set ;

coherence

for b_{1} being Subset-Family of X st b_{1} is diff-finite-partition-closed holds

b_{1} is diff-c=-finite-partition-closed
by Thm2;

end;
coherence

for b

b

registration

let X be set ;

ex b_{1} being Subset-Family of X st

( b_{1} is diff-c=-finite-partition-closed & b_{1} is diff-finite-partition-closed & b_{1} is cap-finite-partition-closed & b_{1} is with_empty_element )

end;
cluster with_empty_element cap-finite-partition-closed diff-finite-partition-closed diff-c=-finite-partition-closed for Subset-Family of X;

existence ex b

( b

proof end;

theorem :: SRINGS_1:10

for X being set

for S being diff-finite-partition-closed Subset-Family of X holds { (union x) where x is finite Subset of S : x is mutually-disjoint } is diff-closed

for S being diff-finite-partition-closed Subset-Family of X holds { (union x) where x is finite Subset of S : x is mutually-disjoint } is diff-closed

proof end;

theorem Thm5: :: SRINGS_1:11

for X being set

for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X

for A being Element of S

for Q being finite Subset of S st union Q c= A & Q is a_partition of union Q holds

ex R being finite Subset of S st

( union R misses union Q & Q \/ R is a_partition of A )

for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X

for A being Element of S

for Q being finite Subset of S st union Q c= A & Q is a_partition of union Q holds

ex R being finite Subset of S st

( union R misses union Q & Q \/ R is a_partition of A )

proof end;

theorem Thm6: :: SRINGS_1:12

for X being set

for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X holds S is diff-finite-partition-closed

for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X holds S is diff-finite-partition-closed

proof end;

registration

let X be set ;

for b_{1} being cap-finite-partition-closed Subset-Family of X st b_{1} is diff-c=-finite-partition-closed holds

b_{1} is diff-finite-partition-closed
by Thm6;

end;
cluster cap-finite-partition-closed diff-c=-finite-partition-closed -> cap-finite-partition-closed diff-finite-partition-closed for Subset-Family of X;

coherence for b

b

Lem9: for X being set

for S being cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X

for SM, T being FinSequence of S ex P being finite Subset of S st P is a_partition of (meet (rng SM)) \ (Union T)

proof end;

theorem Thm3: :: SRINGS_1:13

for X being set

for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X

for SM, T being finite Subset of S ex P being finite Subset of S st P is a_partition of (meet SM) \ (union T)

for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X

for SM, T being finite Subset of S ex P being finite Subset of S st P is a_partition of (meet SM) \ (union T)

proof end;

Lem10: for X being set

for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X

for SM being FinSequence of S ex P being finite Subset of S st

( P is a_partition of Union SM & ( for n being Nat st n in dom SM holds

SM . n = union { s where s is Element of S : ( s in P & s c= SM . n ) } ) )

proof end;

theorem Thm87: :: SRINGS_1:14

for X being set

for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X

for SM being finite Subset of S ex P being finite Subset of S st

( P is a_partition of union SM & ( for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) } ) )

for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X

for SM being finite Subset of S ex P being finite Subset of S st

( P is a_partition of union SM & ( for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) } ) )

proof end;

Lem11: for X being set

for S being cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X

for SM being Function of NATPLUS,S

for n being NatPlus

for x being set st x in SM . n holds

ex n0 being NatPlus ex np being Nat st

( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) )

proof end;

theorem Thm4: :: SRINGS_1:15

for X being set

for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X

for SM being Function of NATPLUS,S ex P being countable Subset of S st

( P is a_partition of Union SM & ( for n being NatPlus holds Union (SM | (Seg n)) = union { s where s is Element of S : ( s in P & s c= Union (SM | (Seg n)) ) } ) )

for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X

for SM being Function of NATPLUS,S ex P being countable Subset of S st

( P is a_partition of Union SM & ( for n being NatPlus holds Union (SM | (Seg n)) = union { s where s is Element of S : ( s in P & s c= Union (SM | (Seg n)) ) } ) )

proof end;

definition

let X be set ;

let S be Subset-Family of X;

end;
let S be Subset-Family of X;

attr S is with_countable_Cover means :: SRINGS_1:def 4

ex XX being countable Subset of S st XX is Cover of X;

ex XX being countable Subset of S st XX is Cover of X;

:: deftheorem defines with_countable_Cover SRINGS_1:def 4 :

for X being set

for S being Subset-Family of X holds

( S is with_countable_Cover iff ex XX being countable Subset of S st XX is Cover of X );

for X being set

for S being Subset-Family of X holds

( S is with_countable_Cover iff ex XX being countable Subset of S st XX is Cover of X );

Lem6a: for X being set

for S being Subset-Family of X

for XX being Subset of S holds

( union XX = X iff XX is Cover of X )

proof end;

registration

let X be set ;

ex b_{1} being Subset-Family of X st

( b_{1} is diff-c=-finite-partition-closed & b_{1} is diff-finite-partition-closed & b_{1} is cap-finite-partition-closed & b_{1} is with_empty_element & b_{1} is with_countable_Cover )

end;
cluster with_empty_element cap-finite-partition-closed diff-finite-partition-closed diff-c=-finite-partition-closed with_countable_Cover for Subset-Family of X;

existence ex b

( b

proof end;

theorem :: SRINGS_1:16

for X being set

for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X st S is with_countable_Cover holds

ex P being countable Subset of S st P is a_partition of X

for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X st S is with_countable_Cover holds

ex P being countable Subset of S st P is a_partition of X

proof end;

definition

let X be set ;

mode semiring_of_sets of X is with_empty_element cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X;

end;
mode semiring_of_sets of X is with_empty_element cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X;

LemPO: for X being set

for S being Subset of X

for A being Element of S holds union ((PARTITIONS A) /\ (Fin S)) is with_non-empty_elements

proof end;

theorem ThmVAL0: :: SRINGS_1:17

for X being set

for S being cap-finite-partition-closed Subset-Family of X

for A being Element of S holds { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is cap-finite-partition-closed Subset-Family of A

for S being cap-finite-partition-closed Subset-Family of X

for A being Element of S holds { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is cap-finite-partition-closed Subset-Family of A

proof end;

theorem ThmVAL2: :: SRINGS_1:18

for X being set

for S being cap-finite-partition-closed Subset-Family of X

for A being Element of S holds { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is diff-c=-finite-partition-closed Subset-Family of A

for S being cap-finite-partition-closed Subset-Family of X

for A being Element of S holds { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is diff-c=-finite-partition-closed Subset-Family of A

proof end;

theorem Thm99: :: SRINGS_1:19

for X being set

for S being cap-finite-partition-closed Subset-Family of X

for A being Element of S holds

( union ((PARTITIONS A) /\ (Fin S)) is cap-finite-partition-closed diff-finite-partition-closed Subset-Family of A & union ((PARTITIONS A) /\ (Fin S)) is with_non-empty_elements )

for S being cap-finite-partition-closed Subset-Family of X

for A being Element of S holds

( union ((PARTITIONS A) /\ (Fin S)) is cap-finite-partition-closed diff-finite-partition-closed Subset-Family of A & union ((PARTITIONS A) /\ (Fin S)) is with_non-empty_elements )

proof end;

theorem :: SRINGS_1:20

for X being set

for S being cap-finite-partition-closed Subset-Family of X

for A being Element of S holds {{}} \/ (union ((PARTITIONS A) /\ (Fin S))) is semiring_of_sets of A

for S being cap-finite-partition-closed Subset-Family of X

for A being Element of S holds {{}} \/ (union ((PARTITIONS A) /\ (Fin S))) is semiring_of_sets of A

proof end;

theorem thmCup: :: SRINGS_1:21

for X being set

for S being cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X holds { (union x) where x is finite Subset of S : x is mutually-disjoint } is cup-closed

for S being cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X holds { (union x) where x is finite Subset of S : x is mutually-disjoint } is cup-closed

proof end;

theorem :: SRINGS_1:22

for X being set

for S being cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X holds { (union x) where x is finite Subset of S : x is mutually-disjoint } is Ring_of_sets

for S being cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X holds { (union x) where x is finite Subset of S : x is mutually-disjoint } is Ring_of_sets

proof end;