:: $\sigma$-ring and $\sigma$-algebra of Sets
:: by Noboru Endou , Kazuhisa Nakasho and Yasunari Shidama
::
:: Received February 18, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


theorem Lem10: :: SRINGS_3:1
for f1, f2 being FinSequence
for k being Nat st k in Seg ((len f1) * (len f2)) holds
( ((k -' 1) mod (len f2)) + 1 in dom f2 & ((k -' 1) div (len f2)) + 1 in dom f1 )
proof end;

theorem CANFS: :: SRINGS_3:2
for S being non empty finite set holds Union (canFS S) = union S
proof end;

theorem TTT1: :: SRINGS_3:3
for x being object holds <*x*> is disjoint_valued FinSequence
proof end;

theorem Disjoint2: :: SRINGS_3:4
for x, y being set
for F being FinSequence st F = <*x,y*> & x misses y holds
F is disjoint_valued
proof end;

theorem TT1: :: SRINGS_3:5
for f1, f2 being FinSequence ex f being FinSequence st
( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds
f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) )
proof end;

theorem TT2: :: SRINGS_3:6
for f1, f2 being disjoint_valued FinSequence ex f being disjoint_valued FinSequence st
( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds
f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) )
proof end;

theorem NE: :: SRINGS_3:7
for X being set
for S being non empty diff-closed Subset-Family of X holds {} in S
proof end;

registration
let X be set ;
cluster non empty diff-closed -> with_empty_element for Element of K6(K6(X));
coherence
for b1 being Subset-Family of X st not b1 is empty & b1 is diff-closed holds
b1 is with_empty_element
proof end;
end;

definition
let IT be set ;
attr IT is semi-diff-closed means :DefSD: :: SRINGS_3:def 1
for X, Y being set st X in IT & Y in IT holds
ex F being disjoint_valued FinSequence of IT st X \ Y = Union F;
end;

:: deftheorem DefSD defines semi-diff-closed SRINGS_3:def 1 :
for IT being set holds
( IT is semi-diff-closed iff for X, Y being set st X in IT & Y in IT holds
ex F being disjoint_valued FinSequence of IT st X \ Y = Union F );

TV1: for X being set holds bool X is semi-diff-closed
proof end;

registration
let X be set ;
cluster K6(X) -> semi-diff-closed ;
coherence
bool X is semi-diff-closed
by TV1;
end;

registration
let X be set ;
cluster non empty cap-closed semi-diff-closed for Element of K6(K6(X));
existence
ex b1 being Subset-Family of X st
( not b1 is empty & b1 is semi-diff-closed & b1 is cap-closed )
proof end;
end;

:: Following cluster gives classical definition of a semiring of sets
registration
let X be set ;
cluster with_empty_element cap-closed semi-diff-closed for Element of K6(K6(X));
existence
ex b1 being Subset-Family of X st
( b1 is with_empty_element & b1 is semi-diff-closed & b1 is cap-closed )
proof end;
end;

definition
let X be set ;
mode Semiring of X is with_empty_element cap-closed semi-diff-closed Subset-Family of X;
end;

theorem Lm1: :: SRINGS_3:8
for X being set
for S being Subset-Family of X
for S1, S2 being set st S1 in S & S2 in S & S is semi-diff-closed holds
ex x being finite Subset of S st x is a_partition of S1 \ S2
proof end;

theorem :: SRINGS_3:9
for X being set
for S being non empty Subset-Family of X st S is semi-diff-closed holds
S is diff-c=-finite-partition-closed
proof end;

theorem th10: :: SRINGS_3:10
for X being set
for S being Subset-Family of X st S is with_empty_element & S is cap-finite-partition-closed & S is diff-c=-finite-partition-closed holds
S is semi-diff-closed
proof end;

registration
cluster diff-closed -> cap-closed semi-diff-closed for set ;
correctness
coherence
for b1 being set st b1 is diff-closed holds
( b1 is semi-diff-closed & b1 is cap-closed )
;
proof end;
end;

registration
let X be set ;
cluster non empty preBoolean for Element of K6(K6(X));
existence
ex b1 being Subset-Family of X st
( not b1 is empty & b1 is preBoolean )
proof end;
end;

registration
cluster non empty preBoolean -> with_empty_element for set ;
correctness
coherence
for b1 being set st not b1 is empty & b1 is preBoolean holds
b1 is with_empty_element
;
proof end;
end;

ExistRing: for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X ex Y being non empty preBoolean Subset-Family of X st Y = meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z }

proof end;

definition
let X be set ;
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X;
func Ring_generated_by S -> non empty preBoolean Subset-Family of X equals :: SRINGS_3:def 2
meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ;
correctness
coherence
meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } is non empty preBoolean Subset-Family of X
;
proof end;
end;

:: deftheorem defines Ring_generated_by SRINGS_3:def 2 :
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds Ring_generated_by S = meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ;

theorem RingGen1: :: SRINGS_3:11
for X being set
for P being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds P c= Ring_generated_by P
proof end;

lemma100: for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for P being set st P = { A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } holds
( P is non empty Subset-Family of X & S c= P )

proof end;

definition
let X be set ;
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X;
func DisUnion S -> non empty Subset-Family of X equals :: SRINGS_3:def 3
{ A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } ;
coherence
{ A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } is non empty Subset-Family of X
by lemma100;
end;

:: deftheorem defines DisUnion SRINGS_3:def 3 :
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds DisUnion S = { A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } ;

theorem :: SRINGS_3:12
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds S c= DisUnion S by lemma100;

theorem lemma101: :: SRINGS_3:13
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds DisUnion S is cap-closed
proof end;

theorem lemma102: :: SRINGS_3:14
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for A, B, P being set st P = DisUnion S & A in P & B in P & A misses B holds
A \/ B in P
proof end;

theorem lemma103: :: SRINGS_3:15
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for A, B being set st A in S & B in S holds
B \ A in DisUnion S
proof end;

theorem lemma104: :: SRINGS_3:16
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for A, B being set st A in S & B in DisUnion S holds
B \ A in DisUnion S
proof end;

theorem lemma105: :: SRINGS_3:17
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for A, B, R being set st R = DisUnion S & A in R & B in R & A <> {} holds
B \ A in R
proof end;

theorem :: SRINGS_3:18
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds Ring_generated_by S = DisUnion S
proof end;

definition
let X be set ;
mode SigmaRing of X -> non empty preBoolean Subset-Family of X means :DefSigmaRing: :: SRINGS_3:def 4
for F being SetSequence of X st rng F c= it holds
Union F in it;
existence
ex b1 being non empty preBoolean Subset-Family of X st
for F being SetSequence of X st rng F c= b1 holds
Union F in b1
proof end;
end;

:: deftheorem DefSigmaRing defines SigmaRing SRINGS_3:def 4 :
for X being set
for b2 being non empty preBoolean Subset-Family of X holds
( b2 is SigmaRing of X iff for F being SetSequence of X st rng F c= b2 holds
Union F in b2 );

LemX: for X being set
for S being SigmaRing of X holds S is sigma-multiplicative

proof end;

registration
let X be set ;
cluster -> sigma-multiplicative for SigmaRing of X;
coherence
for b1 being SigmaRing of X holds b1 is sigma-multiplicative
by LemX;
end;

definition
let X be set ;
let S be Subset-Family of X;
func sigmaring S -> SigmaRing of X means :Defsigmaring: :: SRINGS_3:def 5
( S c= it & ( for Z being set st S c= Z & Z is SigmaRing of X holds
it c= Z ) );
existence
ex b1 being SigmaRing of X st
( S c= b1 & ( for Z being set st S c= Z & Z is SigmaRing of X holds
b1 c= Z ) )
proof end;
correctness
uniqueness
for b1, b2 being SigmaRing of X st S c= b1 & ( for Z being set st S c= Z & Z is SigmaRing of X holds
b1 c= Z ) & S c= b2 & ( for Z being set st S c= Z & Z is SigmaRing of X holds
b2 c= Z ) holds
b1 = b2
;
;
end;

:: deftheorem Defsigmaring defines sigmaring SRINGS_3:def 5 :
for X being set
for S being Subset-Family of X
for b3 being SigmaRing of X holds
( b3 = sigmaring S iff ( S c= b3 & ( for Z being set st S c= Z & Z is SigmaRing of X holds
b3 c= Z ) ) );

theorem :: SRINGS_3:19
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds sigmaring (Ring_generated_by S) = sigmaring S
proof end;

definition
let X be set ;
mode semialgebra_of_sets of X -> with_empty_element cap-closed semi-diff-closed Subset-Family of X means :Def1: :: SRINGS_3:def 6
X in it;
existence
ex b1 being with_empty_element cap-closed semi-diff-closed Subset-Family of X st X in b1
proof end;
end;

:: deftheorem Def1 defines semialgebra_of_sets SRINGS_3:def 6 :
for X being set
for b2 being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds
( b2 is semialgebra_of_sets of X iff X in b2 );

theorem :: SRINGS_3:20
for X being set
for F being Field_Subset of X holds F is semialgebra_of_sets of X by Def1, PROB_1:5;

ExistAlgebra: for X being set
for S being semialgebra_of_sets of X ex Y being Field_Subset of X st Y = meet { Z where Z is Field_Subset of X : S c= Z }

proof end;

definition
let X be set ;
let S be semialgebra_of_sets of X;
func Field_generated_by S -> Field_Subset of X equals :: SRINGS_3:def 7
meet { Z where Z is Field_Subset of X : S c= Z } ;
correctness
coherence
meet { Z where Z is Field_Subset of X : S c= Z } is Field_Subset of X
;
proof end;
end;

:: deftheorem defines Field_generated_by SRINGS_3:def 7 :
for X being set
for S being semialgebra_of_sets of X holds Field_generated_by S = meet { Z where Z is Field_Subset of X : S c= Z } ;

theorem FieldGen1: :: SRINGS_3:21
for X being set
for P being semialgebra_of_sets of X holds P c= Field_generated_by P
proof end;

theorem :: SRINGS_3:22
for X being set
for S being semialgebra_of_sets of X holds Field_generated_by S = DisUnion S
proof end;

theorem :: SRINGS_3:23
for X being non empty set
for S being semialgebra_of_sets of X holds sigma (Field_generated_by S) = sigma S
proof end;

theorem :: SRINGS_3:24
for X, S being set st S is SigmaField of X holds
S is SigmaRing of X
proof end;

theorem :: SRINGS_3:25
for X, S being set st S is SigmaRing of X & X in S holds
S is SigmaField of X
proof end;

theorem :: SRINGS_3:26
for S being Subset-Family of REAL st S = { I where I is Subset of REAL : I is left_open_interval } holds
( S is with_empty_element & S is semi-diff-closed & S is cap-closed )
proof end;

INTERVAL01: for I being Subset of REAL st I = {} holds
I is right_open_interval

proof end;

INTERVAL02: for I, J being Subset of REAL st I is right_open_interval & J is right_open_interval & I meets J holds
ex K, L being Subset of REAL st
( K is right_open_interval & L is right_open_interval & K misses L & I \ J = K \/ L )

proof end;

OOdif: for I, J being Subset of REAL st I is open_interval & J is open_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

COdif: for I, J being Subset of REAL st I is closed_interval & J is open_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

ROdif: for I, J being Subset of REAL st I is right_open_interval & J is open_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

LOdif: for I, J being Subset of REAL st I is left_open_interval & J is open_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

OCdif: for I, J being Subset of REAL st I is open_interval & J is closed_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

CCdif: for I, J being Subset of REAL st I is closed_interval & J is closed_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

RCdif: for I, J being Subset of REAL st I is right_open_interval & J is closed_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

LCdif: for I, J being Subset of REAL st I is left_open_interval & J is closed_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

ORdif: for I, J being Subset of REAL st I is open_interval & J is right_open_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

CRdif: for I, J being Subset of REAL st I is closed_interval & J is right_open_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

RRdif: for I, J being Subset of REAL st I is right_open_interval & J is right_open_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

LRdif: for I, J being Subset of REAL st I is left_open_interval & J is right_open_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

OLdif: for I, J being Subset of REAL st I is open_interval & J is left_open_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

CLdif: for I, J being Subset of REAL st I is closed_interval & J is left_open_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

RLdif: for I, J being Subset of REAL st I is right_open_interval & J is left_open_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

LLdif: for I, J being Subset of REAL st I is left_open_interval & J is left_open_interval & I meets J holds
ex K, L being Interval st
( K misses L & I \ J = K \/ L )

proof end;

INTERVAL03: for I, J being Subset of REAL st I is right_open_interval & J is right_open_interval holds
I /\ J is right_open_interval

proof end;

OOmeet: for I, J being Interval st I is open_interval & J is open_interval & I meets J holds
I /\ J is Interval

proof end;

OCmeet: for I, J being Interval st I is open_interval & J is closed_interval & I meets J holds
I /\ J is Interval

proof end;

ORmeet: for I, J being Interval st I is open_interval & J is right_open_interval & I meets J holds
I /\ J is Interval

proof end;

OLmeet: for I, J being Interval st I is open_interval & J is left_open_interval & I meets J holds
I /\ J is Interval

proof end;

CCmeet: for I, J being Interval st I is closed_interval & J is closed_interval & I meets J holds
I /\ J is Interval

proof end;

CRmeet: for I, J being Interval st I is closed_interval & J is right_open_interval & I meets J holds
I /\ J is Interval

proof end;

CLmeet: for I, J being Interval st I is closed_interval & J is left_open_interval & I meets J holds
I /\ J is Interval

proof end;

RRmeet: for I, J being Interval st I is right_open_interval & J is right_open_interval & I meets J holds
I /\ J is Interval

proof end;

RLmeet: for I, J being Interval st I is right_open_interval & J is left_open_interval & I meets J holds
I /\ J is Interval

proof end;

LLmeet: for I, J being Interval st I is left_open_interval & J is left_open_interval & I meets J holds
I /\ J is Interval

proof end;

theorem :: SRINGS_3:27
for S being Subset-Family of REAL st S = { I where I is Subset of REAL : I is right_open_interval } holds
( S is with_empty_element & S is semi-diff-closed & S is cap-closed )
proof end;

theorem :: SRINGS_3:28
{ I where I is Interval : verum } is semialgebra_of_sets of REAL
proof end;