:: 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{ F₁() -> set , F₂() -> set , F₃( object ) -> set } :

{ F₃(w) where w is Element of F₁() : w in F₂() } is countable

provided

A1: F₂() 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 b₁ being cap-closed Subset-Family of X st b₁ 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 b₁ being cap-closed with_empty_element Subset-Family of X st b₁ 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 b₁ being n -element FinSequence st b₁ 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 b₁ being n -element FinSequence st
for i being Nat st i in Seg n holds
b₁ . 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 b₁ -element FinSequence
for b₃ being b₁ -element FinSequence holds
( b₃ is SemiringFamily of X iff for i being Nat st i in Seg n holds
b₃ . i is semiring_of_sets of (X . i) );

theorem Thm16: :: SRINGS_4:18

for n being non zero Nat
for X being non-empty b₁ -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 b₁ -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 b₁ -element FinSequence st f in product X holds
f is b₁ -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 b₁ being set st
for f being object holds
( f in b₁ iff ex g being Function st
( f = product g & g in product X ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for f being object holds
( f in b₁ iff ex g being Function st
( f = product g & g in product X ) ) ) & ( for f being object holds
( f in b₂ iff ex g being Function st
( f = product g & g in product X ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines SemiringProduct SRINGS_4:def 4 :
for n being non zero Nat
for X being b₁ -element FinSequence
for b₃ being set holds
( b₃ = SemiringProduct X iff for f being object holds
( f in b₃ 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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ being SemiringFamily of X st b₁ 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 b₁ being semiring_of_sets of X st b₁ 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 b₁ -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 b₁ -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 b₁ -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 b₁ being n -element FinSequence st
for i being Nat st i in Seg n holds
b₁ . 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 b₁ -element FinSequence
for b₃ being b₁ -element FinSequence holds
( b₃ is ClassicalSemiringFamily of X iff for i being Nat st i in Seg n holds
b₃ . 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 b₁ -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 b₁ -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;