SRINGS_1: Semiring of Sets

:: Semiring of Sets
:: by Roland Coghetto
::
:: Received March 31, 2014
:: Copyright (c) 2014-2021 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

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

cluster union ((PARTITIONS {}) /\ (Fin S)) -> empty ;

coherence

proof end;

end;

registration

let X be set ;

cluster cobool X -> with_empty_element ;

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

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 :

registration

let X be set ;

cluster cobool X -> cap-finite-partition-closed ;

coherence by Lem4;

end;

registration

let X be set ;

cluster cap-finite-partition-closed for Element of bool (bool X);

existence

proof end;

end;

registration

let X be set ;

cluster cap-closed -> cap-finite-partition-closed for Element of bool (bool X);

coherence

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

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

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 :

registration

let X be set ;

cluster cobool X -> diff-finite-partition-closed ;

coherence by Lem4;

end;

registration

let X be set ;

cluster diff-finite-partition-closed for Element of bool (bool X);

existence

proof end;

end;

registration

let X be set ;

cluster diff-closed -> diff-finite-partition-closed for Element of bool (bool X);

coherence

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

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 :

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 ;

cluster diff-finite-partition-closed -> diff-c=-finite-partition-closed for Element of bool (bool X);

coherence by Thm2;

end;

registration

let X be set ;

cluster cobool X -> diff-c=-finite-partition-closed ;

coherence ;

end;

registration

let X be set ;

cluster with_empty_element cap-finite-partition-closed diff-finite-partition-closed diff-c=-finite-partition-closed for Element of bool (bool X);

existence

proof end;

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

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 ;

cluster cap-finite-partition-closed diff-c=-finite-partition-closed -> cap-finite-partition-closed diff-finite-partition-closed for Element of bool (bool X);

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

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 :

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 ;

cluster cobool X -> with_countable_Cover ;

coherence

proof end;

end;

registration

let X be set ;

cluster with_empty_element cap-finite-partition-closed diff-finite-partition-closed diff-c=-finite-partition-closed with_countable_Cover for Element of bool (bool X);

existence

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

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;

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

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

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 )

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

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

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

proof end;