:: $\sigma$-ring and $\sigma$-algebra of Sets
:: by Noboru Endou , Kazuhisa Nakasho and Yasunari Shidama
::
:: Received February 18, 2015
:: Copyright (c) 2015-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies CARD_1, CARD_3, EQREL_1, FINSET_1, FINSUB_1, FUNCT_1, NUMBERS,
PROB_1, RELAT_1, SETFAM_1, SIMPLEX0, SRINGS_1, SUBSET_1, TARSKI,
XBOOLE_0, ZFMISC_1, ARYTM_1, ARYTM_3, XXREAL_0, PROB_2, FINSEQ_1, NAT_1,
ORDINAL4, INT_1, UPROOTS, SETLIM_2, SRINGS_3, MEASURE5, REAL_1, SUPINF_1,
XXREAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, PROB_1, EQREL_1, SETFAM_1, FINSET_1,
CARD_3, FINSUB_1, FUNCT_1, SIMPLEX0, SRINGS_1, ORDINAL1, NUMBERS,
XXREAL_0, RELSET_1, KURATO_0, XREAL_0, XXREAL_1, XCMPLX_0, NAT_D, PROB_2,
SETLIM_2, SUPINF_1, FINSEQ_1, RCOMP_1, MEASURE5;
constructors SRINGS_1, RELSET_1, PARTIT1, PROB_2, NAT_D, MESFUNC5, SETLIM_2,
KURATO_0, COHSP_1, SUPINF_1, RCOMP_1, MEASURE5;
registrations EQREL_1, FINSET_1, FINSUB_1, MEASURE1, PROB_1, SIMPLEX0,
SRINGS_1, SUBSET_1, XBOOLE_0, XTUPLE_0, ZFMISC_1, MEMBERED, NAT_1,
RELSET_1, XREAL_0, XXREAL_0, FUNCT_1, FINSEQ_1, ROUGHS_1, ORDINAL1,
COHSP_1, MEASURE5, XXREAL_1;
requirements BOOLE, SUBSET, ARITHM, NUMERALS, REAL;
begin :: Preliminaries
theorem :: SRINGS_3:1
for f1,f2 be FinSequence, k be 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;
theorem :: SRINGS_3:2
for S be non empty finite set holds Union canFS S = union S;
theorem :: SRINGS_3:3
for x be object holds <*x*> is disjoint_valued FinSequence;
theorem :: SRINGS_3:4
for x,y be set, F be FinSequence st F = <*x,y*> & x misses y holds
F is disjoint_valued;
theorem :: SRINGS_3:5
for f1,f2 be FinSequence
ex f be FinSequence st
Union f1 /\ Union f2 = Union f &
dom f = Seg (len f1 * len f2) &
for i be Nat st i in dom f holds
f.i = f1.((i-'1) div (len f2) + 1) /\ f2.((i-'1) mod (len f2) + 1);
theorem :: SRINGS_3:6
for f1,f2 be disjoint_valued FinSequence
ex f be disjoint_valued FinSequence st
Union f1 /\ Union f2 = Union f &
dom f = Seg (len f1 * len f2) &
for i be Nat st i in dom f holds
f.i = f1.((i-'1) div (len f2) + 1) /\ f2.((i-'1) mod (len f2) + 1);
theorem :: SRINGS_3:7
for X be set, S be non empty diff-closed Subset-Family of X holds
{} in S;
registration let X be set;
cluster non empty diff-closed -> with_empty_element for Subset-Family of X;
end;
begin :: Classical Semi-ring, Ring and Sigma-ring of Sets
definition
let IT be set;
attr IT is semi-diff-closed means
:: SRINGS_3:def 1
for X,Y being set st X in IT & Y in IT holds
ex F be disjoint_valued FinSequence of IT st X \ Y = Union F;
end;
registration let X be set;
cluster bool X -> semi-diff-closed;
end;
registration
let X be set;
cluster non empty semi-diff-closed cap-closed for Subset-Family of X;
end;
:: Following cluster gives classical definition of a semiring of sets
registration let X be set;
cluster with_empty_element semi-diff-closed cap-closed
for Subset-Family of X;
end;
definition let X be set;
mode Semiring of X is with_empty_element semi-diff-closed cap-closed
Subset-Family of X;
end;
theorem :: SRINGS_3:8
for X be set, S be Subset-Family of X, S1,S2 be set st
S1 in S & S2 in S & S is semi-diff-closed holds
ex x be finite Subset of S st x is a_partition of S1 \ S2;
theorem :: SRINGS_3:9
for X be set, S be non empty Subset-Family of X st
S is semi-diff-closed holds S is diff-c=-finite-partition-closed;
theorem :: SRINGS_3:10
for X be set, S be 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;
registration
cluster diff-closed -> semi-diff-closed cap-closed for set;
end;
registration
let X be set;
cluster non empty preBoolean for Subset-Family of X;
end;
registration
cluster non empty preBoolean -> with_empty_element for set;
end;
definition
let X be set, S be with_empty_element semi-diff-closed
cap-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};
end;
theorem :: SRINGS_3:11
for X being set, P being with_empty_element semi-diff-closed
cap-closed Subset-Family of X
holds P c= Ring_generated_by P;
definition
let X be set,
S be with_empty_element semi-diff-closed cap-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 be disjoint_valued FinSequence of S st A = Union F };
end;
theorem :: SRINGS_3:12
for X being set,
S be with_empty_element semi-diff-closed cap-closed Subset-Family of X
holds
S c= DisUnion S;
theorem :: SRINGS_3:13
for X being set, S being with_empty_element semi-diff-closed cap-closed
Subset-Family of X holds DisUnion S is cap-closed;
theorem :: SRINGS_3:14
for X being set, S being with_empty_element semi-diff-closed cap-closed
Subset-Family of X, A,B,P being set
st P = DisUnion S & A in P & B in P & A misses B
holds A \/ B in P;
theorem :: SRINGS_3:15
for X being set, S being with_empty_element semi-diff-closed cap-closed
Subset-Family of X, A,B being set st A in S & B in S
holds B \ A in DisUnion S;
theorem :: SRINGS_3:16
for X being set, S being with_empty_element semi-diff-closed cap-closed
Subset-Family of X, A,B being set
st A in S & B in DisUnion S
holds B \ A in DisUnion S;
theorem :: SRINGS_3:17
for X being set, S being with_empty_element semi-diff-closed cap-closed
Subset-Family of X, A,B,R being set
st R = DisUnion S & A in R & B in R & A <> {}
holds B \ A in R;
theorem :: SRINGS_3:18
for X being set, S being with_empty_element semi-diff-closed
cap-closed Subset-Family of X holds
Ring_generated_by S = DisUnion S;
definition
let X be set;
mode SigmaRing of X -> non empty preBoolean Subset-Family of X means
:: SRINGS_3:def 4
for F be SetSequence of X st rng F c= it holds Union F in it;
end;
registration let X be set;
cluster -> sigma-multiplicative for SigmaRing of X;
end;
definition let X be set, S be Subset-Family of X;
func sigmaring S -> SigmaRing of X means
:: SRINGS_3:def 5
S c= it & for Z be set st S c= Z & Z is SigmaRing of X holds it c= Z;
end;
theorem :: SRINGS_3:19
for X be set, S be with_empty_element semi-diff-closed
cap-closed Subset-Family of X holds
sigmaring(Ring_generated_by S) = sigmaring S;
begin :: Semi-algebra, Algebra and Sigma-algebra of Sets
definition let X be set;
mode semialgebra_of_sets of X ->
with_empty_element semi-diff-closed cap-closed Subset-Family of X means
:: SRINGS_3:def 6
X in it;
end;
theorem :: SRINGS_3:20
for X being set, F being Field_Subset of X holds
F is semialgebra_of_sets of X;
definition
let X be set, S be semialgebra_of_sets of X;
func Field_generated_by S -> non empty Field_Subset of X equals
:: SRINGS_3:def 7
meet {Z where Z is Field_Subset of X : S c= Z};
end;
theorem :: SRINGS_3:21
for X being set, P being semialgebra_of_sets of X holds
P c= Field_generated_by P;
theorem :: SRINGS_3:22
for X being set, S being semialgebra_of_sets of X holds
Field_generated_by S = DisUnion S;
theorem :: SRINGS_3:23
for X being non empty set, S being semialgebra_of_sets of X holds
sigma (Field_generated_by S) = sigma S;
begin :: Mutual Relationship of between Sigma-ring and Sigma-algebra of Sets
theorem :: SRINGS_3:24
for X be set, S be set st S is SigmaField of X holds S is SigmaRing of X;
theorem :: SRINGS_3:25
for X be set, S be set st S is SigmaRing of X & X in S holds
S is SigmaField of X;
theorem :: SRINGS_3:26
for S be Subset-Family of REAL
st S = { I where I is Subset of REAL : I is left_open_interval }
holds S is with_empty_element semi-diff-closed cap-closed;
theorem :: SRINGS_3:27
for S be Subset-Family of REAL
st S = { I where I is Subset of REAL : I is right_open_interval }
holds S is with_empty_element semi-diff-closed cap-closed;
theorem :: SRINGS_3:28
the set of all I where I is Interval
is semialgebra_of_sets of REAL;