:: Finite Product of Semiring of Sets
::  by Roland Coghetto
::
:: Received April 19, 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 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

::$CT

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;