:: Semiring of Sets
:: by Roland Coghetto
::
:: Received March 31, 2014
:: Copyright (c) 2014-2019 Association of Mizar Users

theorem Lem1: :: SRINGS_1:1
for X, Y being set holds (X \/ Y) \ (Y \ X) = X
proof end;

registration
let X be set ;
let S be Subset-Family of X;
let S1, S2 be finite Subset of S;
cluster INTERSECTION (S1,S2) -> finite ;
coherence
INTERSECTION (S1,S2) is finite
proof end;
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 (() /\ (Fin S)) } = union (() /\ (Fin S))
proof end;

A4bis:
proof end;

registration
let X be set ;
let S be Subset-Family of X;
cluster union (() /\ (Fin S)) -> empty ;
coherence
union (() /\ (Fin S)) is empty
proof end;
end;

registration
let X be set ;
coherence
proof end;
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 () 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 () 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 () st P is a_partition of A \ B ) & {X} is countable Subset of () & 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;

theorem thmIL: :: SRINGS_1:3
for X being set st X is cap-closed & X is cup-closed holds
X is Ring_of_sets
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;
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;
end;

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

registration
let X be set ;
coherence by Lem4;
end;

registration
let X be set ;
existence
ex b1 being Subset-Family of X st b1 is cap-finite-partition-closed
proof end;
end;

registration
let X be set ;
coherence
for b1 being Subset-Family of X st b1 is cap-closed holds
b1 is cap-finite-partition-closed
proof end;
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 )
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 () /\ ()
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
proof end;

theorem Thm86: :: SRINGS_1:7
for X being set
for S being cap-finite-partition-closed Subset-Family of X holds { () 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;
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;
end;

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

registration
let X be set ;
coherence by Lem4;
end;

registration
let X be set ;
existence
ex b1 being Subset-Family of X st b1 is diff-finite-partition-closed
proof end;
end;

registration
let X be set ;
coherence
for b1 being Subset-Family of X st b1 is diff-closed holds
b1 is diff-finite-partition-closed
proof end;
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 \ ()
proof end;

definition
let X be set ;
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;
end;

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

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
proof end;

registration
let X be set ;
coherence
for b1 being Subset-Family of X st b1 is diff-finite-partition-closed holds
b1 is diff-c=-finite-partition-closed
by Thm2;
end;

registration
let X be set ;
coherence ;
end;

registration
let X be set ;
existence
ex b1 being Subset-Family of X st
( b1 is diff-c=-finite-partition-closed & b1 is diff-finite-partition-closed & b1 is cap-finite-partition-closed & b1 is with_empty_element )
proof end;
end;

theorem :: SRINGS_1:10
for X being set
for S being diff-finite-partition-closed Subset-Family of X holds { () 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 )
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
proof end;

registration
let X be set ;
coherence
for b1 being cap-finite-partition-closed Subset-Family of X st b1 is diff-c=-finite-partition-closed holds
b1 is diff-finite-partition-closed
by Thm6;
end;

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

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) \ ()
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 ) } ) )
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)) ) } ) )
proof end;

definition
let X be set ;
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;
end;

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

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 ;
coherence
proof end;
end;

registration
let X be set ;
existence
ex b1 being Subset-Family of X st
( b1 is diff-c=-finite-partition-closed & b1 is diff-finite-partition-closed & b1 is cap-finite-partition-closed & b1 is with_empty_element & b1 is with_countable_Cover )
proof end;
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
proof end;

definition end;

LemPO: for X being set
for S being Subset of X
for A being Element of S holds union (() /\ (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 (() /\ (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 (() /\ (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 (() /\ (Fin S)) is cap-finite-partition-closed diff-finite-partition-closed Subset-Family of A & union (() /\ (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 (() /\ (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 { () 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 { () where x is finite Subset of S : x is mutually-disjoint } is Ring_of_sets
proof end;