:: $\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 b₁ being Subset-Family of X st not b₁ is empty & b₁ is diff-closed holds
b₁ 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 b₁ being Subset-Family of X st
( not b₁ is empty & b₁ is semi-diff-closed & b₁ 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 b₁ being Subset-Family of X st
( b₁ is with_empty_element & b₁ is semi-diff-closed & b₁ 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 b₁ being set st b₁ is diff-closed holds
( b₁ is semi-diff-closed & b₁ is cap-closed );

proof end;

end;

registration

let X be set ;

cluster non empty preBoolean for Element of K6(K6(X));

existence
ex b₁ being Subset-Family of X st
( not b₁ is empty & b₁ is preBoolean )

proof end;

end;

registration

cluster non empty preBoolean -> with_empty_element for set ;

correctness
coherence
for b₁ being set st not b₁ is empty & b₁ is preBoolean holds
b₁ 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 b₁ being non empty preBoolean Subset-Family of X st
for F being SetSequence of X st rng F c= b₁ holds
Union F in b₁

proof end;

end;

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

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 b₁ being SigmaRing of X holds b₁ 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 b₁ being SigmaRing of X st
( S c= b₁ & ( for Z being set st S c= Z & Z is SigmaRing of X holds
b₁ c= Z ) )

proof end;

correctness
uniqueness
for b₁, b₂ being SigmaRing of X st S c= b₁ & ( for Z being set st S c= Z & Z is SigmaRing of X holds
b₁ c= Z ) & S c= b₂ & ( for Z being set st S c= Z & Z is SigmaRing of X holds
b₂ c= Z ) holds
b₁ = b₂;
;

end;

:: deftheorem Defsigmaring defines sigmaring SRINGS_3:def 5 :
for X being set
for S being Subset-Family of X
for b₃ being SigmaRing of X holds
( b₃ = sigmaring S iff ( S c= b₃ & ( for Z being set st S c= Z & Z is SigmaRing of X holds
b₃ 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 b₁ being with_empty_element cap-closed semi-diff-closed Subset-Family of X st X in b₁

proof end;

end;

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

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;