:: Semiring of Sets :: by Roland Coghetto :: :: Received March 31, 2014 :: Copyright (c) 2014-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 ARYTM_1, ARYTM_3, CARD_3, EQREL_1, FINSEQ_1, FINSET_1, FINSUB_1, FUNCT_1, NAT_1, NAT_LAT, NUMBERS, ORDINAL1, ORDINAL4, RELAT_1, SETFAM_1, SIMPLEX0, SRINGS_1, SUBSET_1, TARSKI, TAXONOM2, XBOOLE_0, XCMPLX_0, XXREAL_0, ZFMISC_1, CARD_1, LATTICE7, PARTIT1, TEX_1; notations TARSKI, XBOOLE_0, SUBSET_1, EQREL_1, SETFAM_1, FINSET_1, ORDINAL1, CARD_3, RELAT_1, ZFMISC_1, FINSUB_1, FUNCT_1, SIMPLEX0, FINSEQ_1, NUMBERS, XXREAL_0, FUNCT_2, NAT_LAT, XXREAL_3, RELSET_1, TAXONOM2, NAT_1, TEX_1, LATTICE7, PARTIT1, CARD_1; constructors LATTICE5, NAT_LAT, RELSET_1, MEASURE6, TAXONOM2, COHSP_1, LATTICE7, PARTIT1, TOPGEN_4, TEX_1; registrations CARD_3, EQREL_1, FINSEQ_1, FINSET_1, FUNCT_1, INT_1, MEMBERED, NAT_1, NAT_LAT, RELAT_1, RELSET_1, SIMPLEX0, SUBSET_1, XBOOLE_0, XREAL_0, XXREAL_0, XXREAL_3, SETFAM_1, COHSP_1, ORDINAL1, CARD_1, ZFMISC_1; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; begin :: Preliminaries reserve X for set; reserve S for Subset-Family of X; theorem :: SRINGS_1:1 for X,Y be set holds (X\/Y)\(Y\X)=X; registration let X,S; let S1,S2 be finite Subset of S; cluster INTERSECTION(S1,S2) -> finite; end; theorem :: SRINGS_1:2 for S be Subset-Family of X, A be Element of S holds {x where x is Element of S: x in union (PARTITIONS(A)/\Fin S)} = union (PARTITIONS(A)/\Fin S); registration let X,S; cluster union (PARTITIONS({})/\Fin S) -> empty; end; registration let X; cluster cobool X -> with_empty_element; end; theorem :: SRINGS_1:3 for X be set st X is cap-closed cup-closed holds X is Ring_of_sets; begin definition let X be set; let S be Subset-Family of X; attr S is cap-finite-partition-closed means :: SRINGS_1:def 1 for S1,S2 be Element of S st S1/\S2 is non empty ex x be finite Subset of S st x is a_partition of S1/\S2; end; registration let X be set; cluster cobool X -> cap-finite-partition-closed; end; registration let X be set; cluster cap-finite-partition-closed for Subset-Family of X; end; registration let X be set; cluster cap-closed -> cap-finite-partition-closed for Subset-Family of X; end; theorem :: SRINGS_1:4 for A be non empty set, S be cap-finite-partition-closed Subset-Family of X, P1,P2 be a_partition of A st P1 is finite Subset of S & P2 is finite Subset of S ex P be a_partition of A st P is finite Subset of S & P '<' P1 '/\' P2; theorem :: SRINGS_1:5 for S be cap-finite-partition-closed Subset-Family of X holds for A,B be finite Subset of S st A is mutually-disjoint & B is mutually-disjoint ex P be finite Subset of S st P is a_partition of union A /\ union B; theorem :: SRINGS_1:6 for S be cap-finite-partition-closed Subset-Family of X holds for SM be finite Subset of S ex P be finite Subset of S st P is a_partition of meet SM; theorem :: SRINGS_1:7 for S be cap-finite-partition-closed Subset-Family of X holds {union x where x is finite Subset of S:x is mutually-disjoint} is cap-closed; definition let X be set; let S be Subset-Family of X; attr S is diff-finite-partition-closed means :: SRINGS_1:def 2 for S1,S2 be Element of S st S1\S2 is non empty ex x be finite Subset of S st x is a_partition of S1\S2; end; registration let X be set; cluster cobool X -> diff-finite-partition-closed; end; registration let X be set; cluster diff-finite-partition-closed for Subset-Family of X; end; registration let X be set; cluster diff-closed -> diff-finite-partition-closed for Subset-Family of X; end; theorem :: SRINGS_1:8 for S be diff-finite-partition-closed Subset-Family of X, S1 be Element of S, T be finite Subset of S holds ex P be finite Subset of S st P is a_partition of S1 \ union T; begin :: Partitions in a Difference of Sets definition let X be set; let S be Subset-Family of X; attr S is diff-c=-finite-partition-closed means :: SRINGS_1:def 3 for S1,S2 be Element of S st S2 c= S1 holds ex x be finite Subset of S st x is a_partition of S1\S2; end; theorem :: SRINGS_1:9 for S be Subset-Family of X st S is diff-finite-partition-closed holds S is diff-c=-finite-partition-closed; registration let X; cluster diff-finite-partition-closed -> diff-c=-finite-partition-closed for Subset-Family of X; end; registration let X; cluster cobool X -> diff-c=-finite-partition-closed; end; registration let X; cluster diff-c=-finite-partition-closed diff-finite-partition-closed cap-finite-partition-closed with_empty_element for Subset-Family of X; end; theorem :: SRINGS_1:10 for S be diff-finite-partition-closed Subset-Family of X holds {union x where x is finite Subset of S:x is mutually-disjoint} is diff-closed; theorem :: SRINGS_1:11 for S be cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X holds (for A be Element of S, Q be finite Subset of S st union Q c= A & Q is a_partition of union Q ex R be finite Subset of S st union R misses union Q & Q\/R is a_partition of A); theorem :: SRINGS_1:12 for S be diff-c=-finite-partition-closed cap-finite-partition-closed Subset-Family of X holds S is diff-finite-partition-closed; registration let X be set; cluster diff-c=-finite-partition-closed -> diff-finite-partition-closed for cap-finite-partition-closed Subset-Family of X; end; theorem :: SRINGS_1:13 for S be cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X, SM,T be finite Subset of S holds ex P be finite Subset of S st P is a_partition of (meet SM) \ union T; theorem :: SRINGS_1:14 for S be cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X, SM be finite Subset of S holds ex P be finite Subset of S st P is a_partition of union SM & for Y be Element of SM holds Y=union {s where s is Element of S:s in P & s c= Y}; theorem :: SRINGS_1:15 for S be cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X,SM be Function of NATPLUS,S holds ex P be countable Subset of S st P is a_partition of Union SM & for n be NatPlus holds Union (SM|Seg n)= union{s where s is Element of S: s in P & s c= Union (SM|Seg n)}; begin :: Countable Covers definition let X be set; let S be Subset-Family of X; attr S is with_countable_Cover means :: SRINGS_1:def 4 ex XX be countable Subset of S st XX is Cover of X; end; registration let X; cluster cobool X -> with_countable_Cover; end; registration let X; cluster diff-c=-finite-partition-closed diff-finite-partition-closed cap-finite-partition-closed with_empty_element with_countable_Cover for Subset-Family of X; end; theorem :: SRINGS_1:16 for S be cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X st S is with_countable_Cover holds ex P be countable Subset of S st P is a_partition of X; definition let X be set; mode semiring_of_sets of X is cap-finite-partition-closed diff-c=-finite-partition-closed with_empty_element Subset-Family of X; end; theorem :: SRINGS_1:17 for S be cap-finite-partition-closed Subset-Family of X, A be Element of S holds {x where x is Element of S: x in union (PARTITIONS(A)/\Fin S)} is cap-finite-partition-closed Subset-Family of A; theorem :: SRINGS_1:18 for S be cap-finite-partition-closed Subset-Family of X, A be Element of S holds {x where x is Element of S: x in union (PARTITIONS(A)/\Fin S)} is diff-c=-finite-partition-closed Subset-Family of A; theorem :: SRINGS_1:19 for S be cap-finite-partition-closed Subset-Family of X, A be Element of S holds union (PARTITIONS(A)/\Fin S) is cap-finite-partition-closed diff-finite-partition-closed Subset-Family of A & union (PARTITIONS(A)/\Fin S) is with_non-empty_elements; theorem :: SRINGS_1:20 for S be cap-finite-partition-closed Subset-Family of X, A be Element of S holds {{}}\/union (PARTITIONS(A)/\Fin S) is semiring_of_sets of A; theorem :: SRINGS_1:21 for S be cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X holds {union x where x is finite Subset of S:x is mutually-disjoint} is cup-closed; theorem :: SRINGS_1:22 for S be cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X holds {union x where x is finite Subset of S:x is mutually-disjoint} is Ring_of_sets;