:: $\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 :: (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, 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, 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;