:: Semiring of Sets: Examples
:: by Roland Coghetto
::
:: Received March 31, 2014
:: Copyright (c) 2014-2019 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;