:: Finite Product of Semiring of Sets
:: by Roland Coghetto
::
:: Received April 19, 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 ARYTM_3, CARD_3, EQREL_1, FINSEQ_1, FINSET_1, FINSUB_1, FUNCT_1,
RELAT_1, SETFAM_1, SIMPLEX0, SRINGS_1, SUBSET_1, TARSKI, XBOOLE_0,
ZFMISC_1, CARD_1, TEX_1, PRE_TOPC, RCOMP_1, STRUCT_0, FUNCT_2, SRINGS_4,
NAT_1, XCMPLX_0, FINSEQ_2, ORDINAL4, XXREAL_0, SRINGS_3;
notations TARSKI, XBOOLE_0, SUBSET_1, EQREL_1, SETFAM_1, FINSET_1, CARD_3,
ZFMISC_1, FINSUB_1, FUNCT_1, SIMPLEX0, CARD_1, STRUCT_0, PRE_TOPC,
BINOP_1, TEX_1, ENUMSET1, ORDINAL1, RELAT_1, RELSET_1, FUNCT_2, XCMPLX_0,
XXREAL_0, SRINGS_1, FINSEQ_1, FINSEQ_2, SRINGS_3;
constructors COHSP_1, SRINGS_1, TEX_1, TOPREALB, SRINGS_3;
registrations FINSET_1, RELAT_1, RELSET_1, SIMPLEX0, SUBSET_1, COHSP_1,
ORDINAL1, ZFMISC_1, STRUCT_0, SRINGS_1, CARD_3, EQREL_1, FINSEQ_1,
FUNCT_1, NAT_1, CARD_1, PRE_TOPC, FUNCT_2, XCMPLX_0, XXREAL_0, FINSEQ_2,
SRINGS_3, SRINGS_2, XBOOLE_0, AOFA_000;
requirements BOOLE, NUMERALS, SUBSET;
begin :: Preliminaries
reserve X1,X2,X3,X4 for set;
theorem :: SRINGS_4:1
((X1 /\ X4) \ (X2 \/ X3)) misses (X1 \ (X2 \/ X3 \/ X4)) &
((X1 /\ X4) \ (X2 \/ X3)) misses ((X1 /\ X3 /\ X4) \ X2) &
(X1 \ (X2 \/ X3 \/ X4)) misses ((X1 /\ X3 /\ X4) \ X2);
theorem :: SRINGS_4:2
(X1 \ X2) \ (X3 \ X4) = (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2);
theorem :: SRINGS_4:3
(X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) =
((X1 /\ X4) \ (X2 \/ X3)) \/
(X1 \ (X2 \/ X3 \/ X4)) \/ ((X1 /\ X3 /\ X4) \ X2);
theorem :: SRINGS_4:4
(X1 \ X2) \ (X3 \ X4) = ((X1 /\ X4) \ (X2 \/ X3)) \/
(X1 \ (X2 \/ X3 \/ X4)) \/ ((X1 /\ X3 /\ X4) \ X2);
theorem :: SRINGS_4:5
union {X1,X2,X3} = X1 \/ X2 \/ X3;
begin :: Image of a Semiring of Sets by an Injective Function
theorem :: SRINGS_4:6
for T,S being set, f being Function of T,S,
G being Subset-Family of T holds
f.:G = {f.:A where A is Subset of T : A in G};
registration
let T,S be set,
f be Function of T,S,
G be finite Subset-Family of T;
cluster f.:G -> finite;
end;
registration
let f be Function, A be countable set;
cluster f.:A -> countable;
end;
scheme :: SRINGS_4:sch 1
FraenkelCountable { A() -> set, X() -> set, F(object) -> set }:
{ F(w) where w is Element of A(): w in X() } is countable
provided
X() is countable;
registration
let T,S be set,
f be Function of T,S,
G be countable Subset-Family of T;
cluster f.:G -> countable;
end;
registration
let X,Y be set,S be with_empty_element Subset-Family of X,
f be Function of X,Y;
cluster f.:S -> with_empty_element;
end;
theorem :: SRINGS_4:7
for X,Y being set,f being Function of X,Y,
SF1,SF2 being Subset-Family of X st SF1 c= SF2
holds f.:SF1 c= f.:SF2;
theorem :: SRINGS_4:8
for X,Y being set,S being cap-closed Subset-Family of X,
f being Function of X,Y st f is one-to-one
holds f.:S is cap-closed Subset-Family of Y;
theorem :: SRINGS_4:9
for X,Y being non empty set,
S being cap-finite-partition-closed Subset-Family of X,
f being Function of X,Y st f is one-to-one
holds f.:S is cap-finite-partition-closed Subset-Family of Y;
theorem :: SRINGS_4:10
for X,Y being non empty set,
S being diff-c=-finite-partition-closed Subset-Family of X,
f being Function of X,Y st f is one-to-one & f.:S is non empty
holds f.:S is diff-c=-finite-partition-closed Subset-Family of Y;
theorem :: SRINGS_4:11
for X,Y being non empty set,
S being diff-finite-partition-closed Subset-Family of X,
f being Function of X,Y st f is one-to-one
holds f.:S is diff-finite-partition-closed Subset-Family of Y;
theorem :: SRINGS_4:12
for X,Y being non empty set,S being semiring_of_sets of X,
f being Function of X,Y st f is one-to-one
holds f.:S is semiring_of_sets of Y;
begin
theorem :: SRINGS_4:13
for X being 1-element FinSequence st X.1 is non empty holds
ex I being Function of X.1, product X st
I is one-to-one & I is onto &
for x being object st x in X.1 holds I.x = <*x*>;
registration
let X be set;
cluster cobool X -> cap-closed;
end;
registration
let X be set;
cluster with_empty_element for cap-closed Subset-Family of X;
end;
registration
let X be set;
cluster cup-closed for with_empty_element cap-closed Subset-Family of X;
end;
registration
let X,Y be non empty set;
cluster DIFFERENCE (X,Y) -> non empty;
end;
theorem :: SRINGS_4:14
for X be set,
S be with_empty_element Subset-Family of X holds
DIFFERENCE (S,S) = the set of all A \ B where A, B is Element of S;
definition
let X be set,
S be with_empty_element Subset-Family of X;
func semidiff S -> Subset-Family of X equals
:: SRINGS_4:def 1
DIFFERENCE (S,S);
end;
theorem :: SRINGS_4:15
for X be set,
S be with_empty_element Subset-Family of X,
x be object st x in semidiff S holds
ex A, B being Element of S st x = A \ B;
registration
let X be set,
S be with_empty_element Subset-Family of X;
cluster semidiff S -> with_empty_element;
end;
registration
let X be set,
S be with_empty_element cap-closed cup-closed Subset-Family of X;
cluster semidiff S -> cap-closed diff-finite-partition-closed;
end;
theorem :: SRINGS_4:16
for X being set,
S being with_empty_element cap-closed cup-closed Subset-Family of X holds
semidiff S is semiring_of_sets of X;
begin :: Classical Semiring of Sets and Topological Space
definition
let T be non empty TopSpace;
func capOpCl T -> Subset-Family of [#]T equals
:: SRINGS_4:def 2
{A /\ B where A, B is Subset of T: A is open & B is closed};
end;
registration
let T be non empty TopSpace;
cluster capOpCl T -> with_empty_element cap-closed
diff-finite-partition-closed;
end;
:: T being Topology
:: { O1 \ O2 : O1 is open, O2 is open} is semiring of sets
theorem :: SRINGS_4:17
for T being non empty TopSpace holds capOpCl T is semiring_of_sets of [#]T;
begin :: Finite Product of SemiringFamily of Sets
registration
let n be Nat;
cluster non-empty for n-element FinSequence;
end;
definition
let n be non zero Nat, X be non-empty n-element FinSequence;
mode SemiringFamily of X -> n-element FinSequence means
:: SRINGS_4:def 3
for i being Nat st i in Seg n holds
it.i is semiring_of_sets of X.i;
end;
reserve n for non zero Nat;
reserve X for non-empty n-element FinSequence;
theorem :: SRINGS_4:18
for S being SemiringFamily of X holds dom S = dom X;
theorem :: SRINGS_4:19
for S being SemiringFamily of X holds
for i be Nat st i in Seg n holds union (S.i) c= X.i;
theorem :: SRINGS_4:20
for f being Function, X be n-element FinSequence st f in product X holds
f is n-element FinSequence;
definition
let n be non zero Nat, X be n-element FinSequence;
func SemiringProduct(X) -> set means
:: SRINGS_4:def 4
for f being object holds f in it iff
ex g being Function st f = product g & g in product X;
end;
theorem :: SRINGS_4:21
for X being n-element FinSequence holds
SemiringProduct(X) c= bool Funcs(dom X, union Union X);
theorem :: SRINGS_4:22
for S being SemiringFamily of X holds
SemiringProduct(S) is Subset-Family of product X;
theorem :: SRINGS_4:23
for X being non-empty 1-element FinSequence holds
product X = the set of all <*x*> where x is Element of X.1;
registration
cluster product <*{}*> -> empty;
end;
theorem :: SRINGS_4:24
for x be non empty set holds
product <*x*> = the set of all <*y*> where y is Element of x;
theorem :: SRINGS_4:25
for X being non-empty 1-element FinSequence, S being SemiringFamily of X
holds
SemiringProduct(S)=the set of all product <*s*> where s is Element of S.1;
theorem :: SRINGS_4:26
for x,y being set holds
product <*x*> /\ product <*y*> = product <*(x/\y)*>;
theorem :: SRINGS_4:27
for x,y being set holds product <*x*> \ product <*y*> = product <*(x\y)*>;
theorem :: SRINGS_4:28
for X being non-empty 1-element FinSequence,
S being SemiringFamily of X holds
the set of all product <*s*> where s is Element of S.1 is
semiring_of_sets of the set of all <*x*> where x is Element of X.1;
theorem :: SRINGS_4:29
for X being non-empty 1-element FinSequence, S being SemiringFamily of X
holds SemiringProduct(S) is semiring_of_sets of product X;
theorem :: SRINGS_4:30
for X1,X2 being set, S1 being semiring_of_sets of X1,
S2 being semiring_of_sets of X2 holds
the set of all [:s1,s2:] where s1 is Element of S1,
s2 is Element of S2 is semiring_of_sets of [:X1,X2:];
theorem :: SRINGS_4:31
for Xn being non-empty n-element FinSequence,
X1 being non-empty 1-element FinSequence,
Sn being SemiringFamily of Xn,
S1 be SemiringFamily of X1 st
SemiringProduct(Sn) is semiring_of_sets of product Xn &
SemiringProduct(S1) is semiring_of_sets of product X1 holds
for S12 being Subset-Family of [:product Xn,product X1:] st
S12 = the set of all [:s1,s2:] where
s1 is Element of SemiringProduct(Sn),
s2 is Element of SemiringProduct(S1)
holds
ex I being Function of [: product Xn,product X1 :],product(Xn^X1)
st I is one-to-one & I is onto &
(for x,y be FinSequence st x in product Xn & y in product X1 holds
I.(x,y) = x^y) & I.:S12 = SemiringProduct(Sn^S1);
theorem :: SRINGS_4:32
for Xn being non-empty n-element FinSequence,
X1 being non-empty 1-element FinSequence,
Sn being SemiringFamily of Xn, S1 be SemiringFamily of X1 st
SemiringProduct(Sn) is semiring_of_sets of product Xn &
SemiringProduct(S1) is semiring_of_sets of product X1 holds
SemiringProduct(Sn^S1) is semiring_of_sets of product (Xn^X1);
:: Product of n semiring of sets is semiring of sets
theorem :: SRINGS_4:33
for S being SemiringFamily of X holds
SemiringProduct(S) is semiring_of_sets of product X;
definition
let n be non zero Nat,
X be non-empty n-element FinSequence,
S be SemiringFamily of X;
attr S is cap-closed-yielding means
:: SRINGS_4:def 5
for i being Nat st i in Seg n holds S.i is cap-closed;
end;
registration
let n be non zero Nat, X be non-empty n-element FinSequence;
cluster cap-closed-yielding for SemiringFamily of X;
end;
begin :: Finite Product of Classical Semiring of Sets
registration
let X being set;
cluster cap-closed for semiring_of_sets of X;
end;
theorem :: SRINGS_4:34
for X being non-empty 1-element FinSequence,
S being cap-closed-yielding SemiringFamily of X holds
the set of all product <*s*> where s is Element of S.1 is
cap-closed semiring_of_sets of the set of all <*x*> where x is Element of X.1
;
theorem :: SRINGS_4:35
for X being non-empty 1-element FinSequence,
S being cap-closed-yielding SemiringFamily of X
holds SemiringProduct(S) is cap-closed semiring_of_sets of product X;
theorem :: SRINGS_4:36
for X1,X2 being set, S1 being cap-closed semiring_of_sets of X1,
S2 being cap-closed semiring_of_sets of X2 holds
the set of all [:s1,s2:] where s1 is Element of S1,
s2 is Element of S2 is cap-closed semiring_of_sets of [:X1,X2:];
theorem :: SRINGS_4:37
for Xn being non-empty n-element FinSequence,
X1 being non-empty 1-element FinSequence,
Sn being cap-closed-yielding SemiringFamily of Xn,
S1 be cap-closed-yielding SemiringFamily of X1 st
SemiringProduct(Sn) is cap-closed semiring_of_sets of product Xn &
SemiringProduct(S1) is cap-closed semiring_of_sets of product X1 holds
SemiringProduct(Sn^S1) is cap-closed semiring_of_sets of product (Xn^X1);
registration
let n, X;
let S be cap-closed-yielding SemiringFamily of X;
cluster SemiringProduct(S) -> cap-closed;
end;
:: Product of n classical semirings of sets is classical semiring of sets
theorem :: SRINGS_4:38
for S being cap-closed-yielding SemiringFamily of X holds
SemiringProduct(S) is cap-closed semiring_of_sets of product X;
begin :: Measurable Rectangle
:: n-classical semiring of sets
definition
let n be non zero Nat, X be non-empty n-element FinSequence;
mode ClassicalSemiringFamily of X -> n-element FinSequence means
:: SRINGS_4:def 6
for i being Nat st i in Seg n holds
it.i is with_empty_element semi-diff-closed cap-closed Subset-Family of X.i;
end;
:: Measurable rectangle
:: p148
:: Charalambos D. Aliprantis Kim C. Border
:: Infinite Dimensional Analysis
:: A Hitchhiker.s Guide Third Edition
:: Springer-Verlag Berlin Heidelberg 1999, 2006
::
:: Synonym SemiringProduct = MeasurableRectangle
::
:: This definition is similary of SemiringProduct
notation
let n be non zero Nat, X be n-element FinSequence;
synonym MeasurableRectangle(X) for SemiringProduct(X);
end;
theorem :: SRINGS_4:39
for S being ClassicalSemiringFamily of X holds
S is cap-closed-yielding SemiringFamily of X;
:: finite product of classical semiring of sets is classical semiring of sets ::
:: Version SRING_3 ::
theorem :: SRINGS_4:40
for S being ClassicalSemiringFamily of X holds
MeasurableRectangle(S) is
with_empty_element semi-diff-closed cap-closed Subset-Family of product X;