:: Semiring of Sets: Examples :: by Roland Coghetto :: :: Received March 31, 2014 :: Copyright (c) 2014-2018 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, MCART_1, NUMBERS, PROB_1, RELAT_1, SETFAM_1, SIMPLEX0, SRINGS_1, SUBSET_1, TARSKI, XBOOLE_0, ZFMISC_1, ARYTM_1, ARYTM_3, COMPLEX1, MEASURE5, ORDINAL1, REAL_1, SUPINF_1, XREAL_0, XXREAL_0, XXREAL_1, SRINGS_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1, SETFAM_1, FINSET_1, CARD_1, CARD_3, RELAT_1, FINSUB_1, PROB_1, FUNCT_1, SIMPLEX0, XTUPLE_0, WELLORD2, MCART_1, SRINGS_1, ORDINAL1, COMPLEX1, NUMBERS, XXREAL_0, XREAL_0, XXREAL_1, XXREAL_3, MEASURE5, RCOMP_1, SUPINF_1, ENUMSET1; constructors SRINGS_1, TOPGEN_4, COMPLEX1, RELSET_1, SIMPLEX0, FINSUB_1, SUPINF_1, RCOMP_1, MEASURE5, TOPGEN_3, ARYTM_2, ENUMSET1, PARTIT1; registrations CARD_1, CARD_3, EQREL_1, FINSET_1, FINSUB_1, MEASURE1, PROB_1, SIMPLEX0, SRINGS_1, SUBSET_1, XBOOLE_0, XTUPLE_0, ZFMISC_1, SETFAM_1, MEMBERED, NAT_1, RELSET_1, XREAL_0, XXREAL_0, XXREAL_1, XXREAL_3; requirements BOOLE, SUBSET, ARITHM, NUMERALS, REAL; begin :: Preliminaries reserve X for set; reserve S for Subset-Family of X; theorem :: SRINGS_2:1 for X1,X2 be set, S1 be Subset-Family of X1, S2 be Subset-Family of X2 holds {[:a,b:] where a is Element of S1, b is Element of S2:a in S1 & b in S2} = {s where s is Subset of [:X1,X2:] : ex a,b be set st a in S1 & b in S2 & s=[:a,b:]}; theorem :: SRINGS_2:2 for X1,X2 be set, S1 be non empty Subset-Family of X1, S2 be non empty Subset-Family of X2 holds {s where s is Subset of [:X1,X2:]: ex x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:]} = the set of all [:x1,x2:] where x1 is Element of S1, x2 is Element of S2; theorem :: SRINGS_2:3 for X1,X2 be set,S1 be Subset-Family of X1,S2 be Subset-Family of X2 st S1 is cap-closed & S2 is cap-closed holds {s where s is Subset of [:X1,X2:]: ex x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:]} is cap-closed; registration let X be set; cluster -> cap-finite-partition-closed diff-c=-finite-partition-closed with_countable_Cover with_empty_element for SigmaField of X; end; begin :: Ordinary Examples of Semirings of Sets theorem :: SRINGS_2:4 for F being SigmaField of X holds F is semiring_of_sets of X; registration let X be set; cluster bool X -> cap-finite-partition-closed diff-c=-finite-partition-closed with_countable_Cover with_empty_element for Subset-Family of X; end; theorem :: SRINGS_2:5 bool X is semiring_of_sets of X; registration let X; cluster Fin X -> cap-finite-partition-closed diff-c=-finite-partition-closed with_empty_element for Subset-Family of X; end; registration let D be denumerable set; cluster Fin D -> with_countable_Cover for Subset-Family of D; end; theorem :: SRINGS_2:6 Fin X is semiring_of_sets of X; theorem :: SRINGS_2:7 for X1,X2 be set, S1 be semiring_of_sets of X1,S2 be semiring_of_sets of X2 holds {s where s is Subset of [:X1,X2:]: ex x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:]} is semiring_of_sets of [:X1,X2:]; theorem :: SRINGS_2:8 for X1,X2 be non empty set, S1 be with_countable_Cover Subset-Family of X1, S2 be with_countable_Cover Subset-Family of X2, S be Subset-Family of [:X1,X2:] st S= {s where s is Subset of [:X1,X2:]: ex x1,x2 be set st x1 in S1 & x2 in S2 & s=[:x1,x2:]} holds S is with_countable_Cover; theorem :: SRINGS_2:9 for S be Subset-Family of REAL st S = {].a,b.] where a,b is Real: a<=b} holds S is cap-closed & S is diff-finite-partition-closed with_empty_element & S is with_countable_Cover; theorem :: SRINGS_2:10 for S be Subset-Family of REAL st S = {s where s is Subset of REAL:s is left_open_interval} holds S is cap-closed & S is diff-finite-partition-closed with_empty_element & S is with_countable_Cover; begin :: Numerical Example definition func sring4_8 -> Subset-Family of {1,2,3,4} equals :: SRINGS_2:def 1 {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}}; end; registration cluster sring4_8 -> with_empty_element; end; registration cluster sring4_8 -> cap-finite-partition-closed non cap-closed; end; registration cluster sring4_8 -> diff-finite-partition-closed; end;