:: Semiring of Sets: Examples
:: by Roland Coghetto
::
:: Received March 31, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users

theorem :: SRINGS_2:1

for X1, X2 being set
for S1 being Subset-Family of X1
for S2 being Subset-Family of X2 holds { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 & b in S2 ) } = { s where s is Subset of [:X1,X2:] : ex a, b being set st
( a in S1 & b in S2 & s = [:a,b:] ) }

proof end;

theorem :: SRINGS_2:2

for X1, X2 being set
for S1 being non empty Subset-Family of X1
for S2 being non empty Subset-Family of X2 holds { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } = { [:x1,x2:] where x1 is Element of S1, x2 is Element of S2 : verum }

proof end;

theorem :: SRINGS_2:3

for X1, X2 being set
for S1 being Subset-Family of X1
for S2 being Subset-Family of X2 st S1 is cap-closed & S2 is cap-closed holds
{ s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } is cap-closed

proof end;

Lem3: for X1, X2 being set
for S1 being Subset-Family of X1
for S2 being Subset-Family of X2 holds { s where s is Subset of [:X1,X2:] : ex s1, s2 being set st
( s1 in S1 & s2 in S2 & s = [:s1,s2:] ) } is Subset-Family of [:X1,X2:]

proof end;

Lem4: for X1, X2, Y1, Y2 being set holds
( [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:(X1 /\ Y1),(X2 \ Y2):] & [:(X1 \ Y1),X2:] misses [:(X1 /\ Y1),(X2 \ Y2):] )

proof end;

Lem6a: for X being set
for S being Subset-Family of X
for XX being Subset of S holds
( union XX = X iff XX is Cover of X )

proof end;

registration

let X be set ;

cluster non empty compl-closed sigma-multiplicative -> cap-finite-partition-closed diff-c=-finite-partition-closed with_countable_Cover with_empty_element for Element of bool (bool X);

coherence
for b₁ being SigmaField of X holds
( b₁ is cap-finite-partition-closed & b₁ is diff-c=-finite-partition-closed & b₁ is with_countable_Cover & b₁ is with_empty_element )

proof end;

end;

theorem :: SRINGS_2:4

for X being set
for F being SigmaField of X holds F is semiring_of_sets of X ;

registration

let X be set ;

cluster bool X -> cap-finite-partition-closed diff-c=-finite-partition-closed with_countable_Cover with_empty_element for Subset-Family of X;

coherence
for b₁ being Subset-Family of X st b₁ = bool X holds
( b₁ is cap-finite-partition-closed & b₁ is diff-c=-finite-partition-closed & b₁ is with_countable_Cover & not b₁ is with_non-empty_elements ) ;

end;

theorem :: SRINGS_2:5

for X being set holds bool X is semiring_of_sets of X ;

Lemme4: for X being set
for a, b, c being object st [a,b] in [:X,(bool X):] & c in X & [a,b] = [c,{c}] holds
( a = c & b = {c} )

proof end;

FinConv: for D being set
for SD being Subset-Family of D holds
( SD = { y where y is Subset of D : y is finite } iff SD = Fin D )

proof end;

registration

let X be set ;

cluster Fin X -> cap-finite-partition-closed diff-c=-finite-partition-closed with_empty_element for Subset-Family of X;

coherence
for b₁ being Subset-Family of X st b₁ = Fin X holds
( b₁ is cap-finite-partition-closed & b₁ is diff-c=-finite-partition-closed & not b₁ is with_non-empty_elements )

proof end;

end;

registration

let D be denumerable set ;

cluster Fin D -> with_countable_Cover for Subset-Family of D;

coherence
for b₁ being Subset-Family of D st b₁ = Fin D holds
b₁ is with_countable_Cover

proof end;

end;

theorem :: SRINGS_2:6

for X being set holds Fin X is semiring_of_sets of X by FINSUB_1:13;

Lemme9: for X1, X2 being non empty set
for S1 being non empty Subset-Family of X1
for S2 being non empty Subset-Family of X2 holds { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 \ {{}} & b in S2 \ {{}} ) } = { s where s is Subset of [:X1,X2:] : ex a, b being set st
( a in S1 \ {{}} & b in S2 \ {{}} & s = [:a,b:] ) }

proof end;

Lem7: for x, S1, S2 being set holds
( x in { [:a,b:] where a is Element of S1 \ {{}}, b is Element of S2 \ {{}} : ( a in S1 \ {{}} & b in S2 \ {{}} ) } iff x in { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 \ {{}} & b in S2 \ {{}} ) } )

proof end;

Lem8: for X1, X2 being non empty set
for S1 being non empty Subset-Family of X1
for S2 being non empty Subset-Family of X2 holds { [:a,b:] where a is Element of S1 \ {{}}, b is Element of S2 \ {{}} : ( a in S1 \ {{}} & b in S2 \ {{}} ) } = { [:a,b:] where a is Element of S1, b is Element of S2 : ( a in S1 \ {{}} & b in S2 \ {{}} ) }

proof end;

Lem9: for X being set
for S being Subset-Family of X
for A being Subset of S holds A is Subset-Family of X

proof end;

theorem :: SRINGS_2:7

for X1, X2 being set
for S1 being semiring_of_sets of X1
for S2 being semiring_of_sets of X2 holds { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } is semiring_of_sets of [:X1,X2:]

proof end;

theorem :: SRINGS_2:8

for X1, X2 being non empty set
for S1 being with_countable_Cover Subset-Family of X1
for S2 being with_countable_Cover Subset-Family of X2
for S being Subset-Family of [:X1,X2:] st S = { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } holds
S is with_countable_Cover

proof end;

THS0: {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } = { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }

proof end;

set II = { ].a,b.] where a, b is Real : a <= b } ;

{ ].a,b.] where a, b is Real : a <= b } c= bool REAL

proof end;

then reconsider II = { ].a,b.] where a, b is Real : a <= b } as Subset-Family of REAL ;

THS2: { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } = II

proof end;

THS1: for S being Subset-Family of REAL st S = {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } holds
( S is cap-closed & S is diff-finite-partition-closed with_empty_element Subset-Family of REAL )

proof end;

LemmA1: II is with_countable_Cover

proof end;

theorem :: SRINGS_2:9

for S being Subset-Family of REAL st S = { ].a,b.] where a, b is Real : a <= b } holds
( S is cap-closed & S is diff-finite-partition-closed & S is with_empty_element & S is with_countable_Cover ) by THS0, THS1, THS2, LemmA1;

LemmB: for S being Subset-Family of REAL st S = { s where s is Subset of REAL : s is left_open_interval } holds
S is with_countable_Cover

proof end;

theorem :: SRINGS_2:10

for S being Subset-Family of REAL st S = { s where s is Subset of REAL : s is left_open_interval } holds
( S is cap-closed & S is diff-finite-partition-closed & S is with_empty_element & S is with_countable_Cover )

proof end;

definition

func sring4_8 -> Subset-Family of {1,2,3,4} equals :: SRINGS_2:def 1
{{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}};

coherence
{{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} is Subset-Family of {1,2,3,4}

proof end;

end;

:: deftheorem defines sring4_8 SRINGS_2:def 1 :
sring4_8 = {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}};

set S = sring4_8 ;

registration

cluster sring4_8 -> with_empty_element ;

coherence
not sring4_8 is with_non-empty_elements

proof end;

end;

LL2: {1,2,3,4} /\ {1,2,3} = {1,2,3}

proof end;

LL3: {1,2,3,4} /\ {2,3,4} = {2,3,4}

proof end;

LL4: {1,2,3,4} /\ {1} = {1}

proof end;

LL5: {1,2,3,4} /\ {2} = {2}

proof end;

LL6: {1,2,3,4} /\ {3} = {3}

proof end;

LL7: {1,2,3,4} /\ {4} = {4}

proof end;

LL10: {1,2,3} /\ {2,3,4} = {2,3}

proof end;

LL11: {1,2,3} /\ {1} = {1}

proof end;

LL12: {1,2,3} /\ {2} = {2}

proof end;

LL13: {1,2,3} /\ {3} = {3}

proof end;

LL14: {1,2,3} /\ {4} = {}

proof end;

LL11a: {2,3,4} /\ {1} = {}

proof end;

LL12a: {2,3,4} /\ {2} = {2}

proof end;

LL13a: {2,3,4} /\ {3} = {3}

proof end;

LL14a: {2,3,4} /\ {4} = {4}

proof end;

LL17: {1} /\ {2} = {}

proof end;

LL18: {1} /\ {3} = {}

proof end;

LL19: {1} /\ {4} = {}

proof end;

LL21: {2} /\ {3} = {}

proof end;

LL22: {2} /\ {4} = {}

proof end;

LL24: {3} /\ {4} = {}

proof end;

Thm1: INTERSECTION (sring4_8,sring4_8) = {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}}

proof end;

LemAA: {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}} = {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} \/ {{2,3}}

proof end;

LemmeA: for x being non empty set st x in sring4_8 holds
( {x} is Subset of sring4_8 & {x} is a_partition of x )

proof end;

Thm98: for x being set st x in sring4_8 holds
ex P being finite Subset of sring4_8 st P is a_partition of x

proof end;

Thm99: ( {{2},{3}} is Subset of sring4_8 & {{2},{3}} is a_partition of {2,3} )

proof end;

LemC: for x being set st x in INTERSECTION (sring4_8,sring4_8) holds
ex P being finite Subset of sring4_8 st P is a_partition of x

proof end;

LemA: not {1,2,3} /\ {2,3,4} in sring4_8

proof end;

registration

cluster sring4_8 -> cap-finite-partition-closed non cap-closed ;

coherence
( sring4_8 is cap-finite-partition-closed & not sring4_8 is cap-closed )

proof end;

end;

GG2: {1,2,3,4} \ {1,2,3} = {4}

proof end;

GG3: {1,2,3,4} \ {2,3,4} = {1}

proof end;

GG4: {1,2,3,4} \ {1} = {2,3,4}

proof end;

GG5: {1,2,3,4} \ {2} = {1,3,4}

proof end;

GG6: {1,2,3,4} \ {3} = {1,2,4}

proof end;

GG7: {1,2,3,4} \ {4} = {1,2,3}

proof end;

GG11: {1,2,3} \ {2,3,4} = {1}

proof end;

GG12: {1,2,3} \ {1} = {2,3}

proof end;

GG13: {1,2,3} \ {2} = {1,3}

proof end;

GG14: {1,2,3} \ {3} = {1,2}

proof end;

GG15: {1,2,3} \ {4} = {1,2,3}

proof end;

GG18: {2,3,4} \ {1,2,3} = {4}

proof end;

GG20: {2,3,4} \ {1} = {2,3,4}

proof end;

GG21: {2,3,4} \ {2} = {3,4}

proof end;

GG22: {2,3,4} \ {3} = {2,4}

proof end;

GG23: {2,3,4} \ {4} = {2,3}

proof end;

GG27: {1} \ {2,3,4} = {1}

proof end;

GG33: {2} \ {1,2,3,4} = {}

proof end;

GG34: {2} \ {1,2,3} = {}

proof end;

GG35: {2} \ {2,3,4} = {}

proof end;

GG41: {3} \ {1,2,3,4} = {}

proof end;

GG42: {3} \ {1,2,3} = {}

proof end;

GG43: {3} \ {2,3,4} = {}

proof end;

GG50: {4} \ {1,2,3} = {4}

proof end;

Thm50: DIFFERENCE (sring4_8,sring4_8) = sring4_8 \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}}

proof end;

ThmV1: ( {{1},{3}} is Subset of sring4_8 & {{1},{3}} is a_partition of {1,3} )

proof end;

ThmV2: ( {{1},{2}} is Subset of sring4_8 & {{1},{2}} is a_partition of {1,2} )

proof end;

ThmV3: ( {{2},{4}} is Subset of sring4_8 & {{2},{4}} is a_partition of {2,4} )

proof end;

ThmV4: ( {{3},{4}} is Subset of sring4_8 & {{3},{4}} is a_partition of {3,4} )

proof end;

ThmV5: ( {{1},{3},{4}} is Subset of sring4_8 & {{1},{3},{4}} is a_partition of {1,3,4} )

proof end;

ThmV6: ( {{1},{2},{4}} is Subset of sring4_8 & {{1},{2},{4}} is a_partition of {1,2,4} )

proof end;

LemD: for x being set st x in DIFFERENCE (sring4_8,sring4_8) holds
ex P being finite Subset of sring4_8 st P is a_partition of x

proof end;

registration

cluster sring4_8 -> diff-finite-partition-closed ;

coherence
sring4_8 is diff-finite-partition-closed

proof end;

end;