:: Finite Product of Semiring of Sets
:: by Roland Coghetto
::
:: Received April 19, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


Thm01: for X1, X2, X3, X4 being set holds
( ((X1 /\ X4) \ (X2 \/ X3)) /\ (X1 \ ((X2 \/ X3) \/ X4)) is empty & ((X1 /\ X4) \ (X2 \/ X3)) /\ (((X1 /\ X3) /\ X4) \ X2) is empty & (X1 \ ((X2 \/ X3) \/ X4)) /\ (((X1 /\ X3) /\ X4) \ X2) is empty )
proof end;

theorem :: SRINGS_4:1
for X1, X2, X3, X4 being set holds
( (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 ) by Thm01;

theorem Thm02: :: SRINGS_4:2
for X1, X2, X3, X4 being set holds (X1 \ X2) \ (X3 \ X4) = (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2)
proof end;

Lm1: for X1, X2, X3, X4 being set holds X1 \ (X2 \/ X3) c= (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)
proof end;

Lm2: for X1, X2, X3, X4 being set holds (X1 /\ X4) \ X2 c= (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)
proof end;

Lm3: for X1, X2, X3, X4 being set holds ((X1 /\ X3) /\ X4) \ X2 c= (X1 /\ X4) \ X2
proof end;

theorem Thm03: :: SRINGS_4:3
for X1, X2, X3, X4 being set holds (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) = (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)
proof end;

theorem Thm04: :: SRINGS_4:4
for X1, X2, X3, X4 being set holds (X1 \ X2) \ (X3 \ X4) = (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)
proof end;

theorem Thm05: :: SRINGS_4:5
for X1, X2, X3 being set holds union {X1,X2,X3} = (X1 \/ X2) \/ X3
proof end;

theorem Thm07: :: SRINGS_4:6
for T, S being set
for f being Function of T,S
for G being Subset-Family of T holds f .: G = { (f .: A) where A is Subset of T : A in G }
proof end;

registration
let T, S be set ;
let f be Function of T,S;
let G be finite Subset-Family of T;
cluster f .: G -> finite ;
coherence
f .: G is finite
proof end;
end;

registration
let f be Function;
let A be countable set ;
cluster f .: A -> countable ;
coherence
f .: A is countable
proof end;
end;

scheme :: SRINGS_4:sch 1
FraenkelCountable{ F1() -> set , F2() -> set , F3( object ) -> set } :
{ F3(w) where w is Element of F1() : w in F2() } is countable
provided
A1: F2() is countable
proof end;

registration
let T, S be set ;
let f be Function of T,S;
let G be countable Subset-Family of T;
cluster f .: G -> countable ;
coherence
f .: G is countable
proof end;
end;

Thm08: for X, Y being set
for S being with_empty_element Subset-Family of X
for f being Function of X,Y holds f .: S is with_empty_element Subset-Family of Y
proof end;

registration
let X, Y be set ;
let S be with_empty_element Subset-Family of X;
let f be Function of X,Y;
cluster f .: S -> with_empty_element ;
coherence
not f .: S is with_non-empty_elements by Thm08;
end;

theorem :: SRINGS_4:7
for X, Y being set
for f being Function of X,Y
for SF1, SF2 being Subset-Family of X st SF1 c= SF2 holds
f .: SF1 c= f .: SF2
proof end;

theorem Thm10: :: SRINGS_4:8
for X, Y being set
for S being cap-closed Subset-Family of X
for f being Function of X,Y st f is one-to-one holds
f .: S is cap-closed Subset-Family of Y
proof end;

theorem Thm11: :: SRINGS_4:9
for X, Y being non empty set
for S being cap-finite-partition-closed Subset-Family of X
for f being Function of X,Y st f is one-to-one holds
f .: S is cap-finite-partition-closed Subset-Family of Y
proof end;

theorem Thm12: :: SRINGS_4:10
for X, Y being non empty set
for S being diff-c=-finite-partition-closed Subset-Family of X
for f being Function of X,Y st f is one-to-one & not f .: S is empty holds
f .: S is diff-c=-finite-partition-closed Subset-Family of Y
proof end;

theorem :: SRINGS_4:11
for X, Y being non empty set
for S being diff-finite-partition-closed Subset-Family of X
for f being Function of X,Y st f is one-to-one holds
f .: S is diff-finite-partition-closed Subset-Family of Y
proof end;

theorem :: SRINGS_4:12
for X, Y being non empty set
for S being semiring_of_sets of X
for f being Function of X,Y st f is one-to-one holds
f .: S is semiring_of_sets of Y by Thm11, Thm12;

theorem :: SRINGS_4:13
canceled;

::$CT
registration
let X be set ;
cluster cobool X -> cap-closed ;
coherence
cobool X is cap-closed
proof end;
end;

registration
let X be set ;
cluster cap-closed cap-finite-partition-closed with_empty_element for Element of bool (bool X);
existence
ex b1 being cap-closed Subset-Family of X st b1 is with_empty_element
proof end;
end;

registration
let X be set ;
cluster non empty cup-closed cap-closed V22() cap-finite-partition-closed with_empty_element for Element of bool (bool X);
existence
ex b1 being cap-closed with_empty_element Subset-Family of X st b1 is cup-closed
proof end;
end;

registration
let X, Y be non empty set ;
cluster DIFFERENCE (X,Y) -> non empty ;
correctness
coherence
not DIFFERENCE (X,Y) is empty ;
proof end;
end;

theorem LemY: :: SRINGS_4:14
for X being set
for S being with_empty_element Subset-Family of X holds DIFFERENCE (S,S) = { (A \ B) where A, B is Element of S : verum }
proof end;

definition
let X be set ;
let S be with_empty_element Subset-Family of X;
func semidiff S -> Subset-Family of X equals :: SRINGS_4:def 1
 DIFFERENCE (S,S);
coherence
DIFFERENCE (S,S) is Subset-Family of X
proof end;
end;

:: deftheorem defines semidiff SRINGS_4:def 1 :
for X being set
for S being with_empty_element Subset-Family of X holds semidiff S = DIFFERENCE (S,S);

theorem LemX1: :: SRINGS_4:15
for X being set
for S being with_empty_element Subset-Family of X
for x being object st x in semidiff S holds
ex A, B being Element of S st x = A \ B
proof end;

registration
let X be set ;
let S be with_empty_element Subset-Family of X;
cluster semidiff S -> with_empty_element ;
coherence
not semidiff S is with_non-empty_elements
proof end;
end;

Thm14: for X being set
for S being cup-closed cap-closed with_empty_element Subset-Family of X holds
( semidiff S is cap-closed & semidiff S is diff-finite-partition-closed )
proof end;

registration
let X be set ;
let S be cup-closed cap-closed with_empty_element Subset-Family of X;
cluster semidiff S -> cap-closed diff-finite-partition-closed ;
coherence
( semidiff S is cap-closed & semidiff S is diff-finite-partition-closed ) by Thm14;
end;

theorem :: SRINGS_4:16
for X being set
for S being cup-closed cap-closed with_empty_element Subset-Family of X holds semidiff S is semiring_of_sets of X ;

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 ) } ;
coherence
{ (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } is Subset-Family of ([#] T)
proof end;
end;

:: deftheorem defines capOpCl SRINGS_4:def 2 :
for T being non empty TopSpace holds capOpCl T = { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } ;

Thm15: for T being non empty TopSpace holds
( capOpCl T is with_empty_element & capOpCl T is cap-closed & capOpCl T is diff-finite-partition-closed )
proof end;

registration
let T be non empty TopSpace;
cluster capOpCl T -> cap-closed diff-finite-partition-closed with_empty_element ;
coherence
( not capOpCl T is with_non-empty_elements & capOpCl T is cap-closed & capOpCl T is diff-finite-partition-closed ) by Thm15;
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) ;

registration
let n be Nat;
cluster Relation-like non-empty K42() -defined Function-like finite n -element FinSequence-like FinSubsequence-like countable for set ;
existence
ex b1 being n -element FinSequence st b1 is non-empty
proof end;
end;

definition
let n be non zero Nat;
let X be non-empty n -element FinSequence;
mode SemiringFamily of X -> n -element FinSequence means :Def2: :: SRINGS_4:def 3
 for i being Nat st i in Seg n holds
it . i is semiring_of_sets of (X . i);
existence
ex b1 being n -element FinSequence st
for i being Nat st i in Seg n holds
b1 . i is semiring_of_sets of (X . i)
proof end;
end;

:: deftheorem Def2 defines SemiringFamily SRINGS_4:def 3 :
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for b3 being b1 -element FinSequence holds
( b3 is SemiringFamily of X iff for i being Nat st i in Seg n holds
b3 . i is semiring_of_sets of (X . i) );

theorem Thm16: :: SRINGS_4:18
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being SemiringFamily of X holds dom S = dom X
proof end;

theorem Thm17: :: SRINGS_4:19
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being SemiringFamily of X
for i being Nat st i in Seg n holds
union (S . i) c= X . i
proof end;

theorem Thm18: :: SRINGS_4:20
for n being non zero Nat
for f being Function
for X being b1 -element FinSequence st f in product X holds
f is b1 -element FinSequence
proof end;

definition
let n be non zero Nat;
let X be n -element FinSequence;
func SemiringProduct X -> set means :Def3: :: 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 ) );
existence
ex b1 being set st
for f being object holds
( f in b1 iff ex g being Function st
( f = product g & g in product X ) )
proof end;
uniqueness
for b1, b2 being set st ( for f being object holds
( f in b1 iff ex g being Function st
( f = product g & g in product X ) ) ) & ( for f being object holds
( f in b2 iff ex g being Function st
( f = product g & g in product X ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines SemiringProduct SRINGS_4:def 4 :
for n being non zero Nat
for X being b1 -element FinSequence
for b3 being set holds
( b3 = SemiringProduct X iff for f being object holds
( f in b3 iff ex g being Function st
( f = product g & g in product X ) ) );

theorem Thm19: :: SRINGS_4:21
for n being non zero Nat
for X being b1 -element FinSequence holds SemiringProduct X c= bool (Funcs ((dom X),(union (Union X))))
proof end;

theorem Thm20: :: SRINGS_4:22
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being SemiringFamily of X holds SemiringProduct S is Subset-Family of (product X)
proof end;

theorem Thm21: :: SRINGS_4:23
for X being non-empty 1 -element FinSequence holds product X = { <*x*> where x is Element of X . 1 : verum }
proof end;

Thm22: product <*{}*> is empty
proof end;

registration
cluster product <*{}*> -> empty ;
coherence
product <*{}*> is empty by Thm22;
end;

theorem Thm23: :: SRINGS_4:24
for x being non empty set holds product <*x*> = { <*y*> where y is Element of x : verum }
proof end;

theorem Thm24: :: SRINGS_4:25
for X being non-empty 1 -element FinSequence
for S being SemiringFamily of X holds SemiringProduct S = { (product <*s*>) where s is Element of S . 1 : verum }
proof end;

theorem Thm25: :: SRINGS_4:26
for x, y being set holds (product <*x*>) /\ (product <*y*>) = product <*(x /\ y)*>
proof end;

theorem Thm26: :: SRINGS_4:27
for x, y being set holds (product <*x*>) \ (product <*y*>) = product <*(x \ y)*>
proof end;

theorem Thm27: :: SRINGS_4:28
for X being non-empty 1 -element FinSequence
for S being SemiringFamily of X holds { (product <*s*>) where s is Element of S . 1 : verum } is semiring_of_sets of { <*x*> where x is Element of X . 1 : verum }
proof end;

theorem Thm28: :: SRINGS_4:29
for X being non-empty 1 -element FinSequence
for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X)
proof end;

theorem Thm29: :: SRINGS_4:30
for X1, X2 being set
for S1 being semiring_of_sets of X1
for S2 being semiring_of_sets of X2 holds { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is semiring_of_sets of [:X1,X2:]
proof end;

theorem Thm30: :: SRINGS_4:31
for n being non zero Nat
for Xn being non-empty b1 -element FinSequence
for X1 being non-empty 1 -element FinSequence
for Sn being SemiringFamily of Xn
for S1 being 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 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } 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 being FinSequence st x in product Xn & y in product X1 holds
I . (x,y) = x ^ y ) & I .: S12 = SemiringProduct (Sn ^ S1) )
proof end;

theorem Thm31: :: SRINGS_4:32
for n being non zero Nat
for Xn being non-empty b1 -element FinSequence
for X1 being non-empty 1 -element FinSequence
for Sn being SemiringFamily of Xn
for S1 being 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))
proof end;

:: Product of n semiring of sets is semiring of sets
theorem Thm32: :: SRINGS_4:33
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X)
proof end;

definition
let n be non zero Nat;
let X be non-empty n -element FinSequence;
let S be SemiringFamily of X;
attr S is cap-closed-yielding means :Def4: :: SRINGS_4:def 5
 for i being Nat st i in Seg n holds
S . i is cap-closed ;
end;

:: deftheorem Def4 defines cap-closed-yielding SRINGS_4:def 5 :
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being SemiringFamily of X holds
( S is cap-closed-yielding iff for i being Nat st i in Seg n holds
S . i is cap-closed );

registration
let n be non zero Nat;
let X be non-empty n -element FinSequence;
cluster non empty Relation-like K42() -defined Function-like finite n -element FinSequence-like FinSubsequence-like countable cap-closed-yielding for SemiringFamily of X;
existence
ex b1 being SemiringFamily of X st b1 is cap-closed-yielding
proof end;
end;

registration
let X be set ;
cluster non empty cap-closed V22() cap-finite-partition-closed diff-finite-partition-closed diff-c=-finite-partition-closed non with_non-empty_elements for Element of bool (bool X);
existence
ex b1 being semiring_of_sets of X st b1 is cap-closed
proof end;
end;

theorem Thm33: :: SRINGS_4:34
for X being non-empty 1 -element FinSequence
for S being cap-closed-yielding SemiringFamily of X holds { (product <*s*>) where s is Element of S . 1 : verum } is cap-closed semiring_of_sets of { <*x*> where x is Element of X . 1 : verum }
proof end;

theorem Thm34: :: SRINGS_4:35
for X being non-empty 1 -element FinSequence
for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed semiring_of_sets of (product X)
proof end;

theorem Thm35: :: SRINGS_4:36
for X1, X2 being set
for S1 being cap-closed semiring_of_sets of X1
for S2 being cap-closed semiring_of_sets of X2 holds { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is cap-closed semiring_of_sets of [:X1,X2:]
proof end;

theorem Thm36: :: SRINGS_4:37
for n being non zero Nat
for Xn being non-empty b1 -element FinSequence
for X1 being non-empty 1 -element FinSequence
for Sn being cap-closed-yielding SemiringFamily of Xn
for S1 being 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))
proof end;

Thm37: for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed
proof end;

registration
let n be non zero Nat;
let X be non-empty n -element FinSequence;
let S be cap-closed-yielding SemiringFamily of X;
cluster SemiringProduct S -> cap-closed ;
coherence
SemiringProduct S is cap-closed by Thm37;
end;

:: Product of n classical semirings of sets is classical semiring of sets
theorem :: SRINGS_4:38
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed semiring_of_sets of (product X) by Thm32;

:: n-classical semiring of sets
definition
let n be non zero Nat;
let X be non-empty n -element FinSequence;
mode ClassicalSemiringFamily of X -> n -element FinSequence means :Def5: :: SRINGS_4:def 6
 for i being Nat st i in Seg n holds
it . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i);
existence
ex b1 being n -element FinSequence st
for i being Nat st i in Seg n holds
b1 . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i)
proof end;
end;

:: deftheorem Def5 defines ClassicalSemiringFamily SRINGS_4:def 6 :
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for b3 being b1 -element FinSequence holds
( b3 is ClassicalSemiringFamily of X iff for i being Nat st i in Seg n holds
b3 . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i) );

notation
let n be non zero Nat;
let X be n -element FinSequence;
synonym MeasurableRectangle X for SemiringProduct X;
end;

theorem Thm38: :: SRINGS_4:39
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being ClassicalSemiringFamily of X holds S is cap-closed-yielding SemiringFamily of X
proof end;

:: finite product of classical semiring of sets is classical semiring of sets ::
:: Version SRING_3 ::
theorem :: SRINGS_4:40
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being ClassicalSemiringFamily of X holds MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X)
proof end;