:: Semiring of Sets: Examples
:: by Roland Coghetto
::
:: Received March 31, 2014
:: Copyright (c) 2014-2018 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 ;
coherence
for b1 being SigmaField of X holds
( b1 is cap-finite-partition-closed & b1 is diff-c=-finite-partition-closed & b1 is with_countable_Cover & b1 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 ;
coherence
for b1 being Subset-Family of X st b1 = bool X holds
( b1 is cap-finite-partition-closed & b1 is diff-c=-finite-partition-closed & b1 is with_countable_Cover & not b1 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 ;
coherence
for b1 being Subset-Family of X st b1 = Fin X holds
( b1 is cap-finite-partition-closed & b1 is diff-c=-finite-partition-closed & not b1 is with_non-empty_elements )
proof end;
end;

registration
let D be denumerable set ;
coherence
for b1 being Subset-Family of D st b1 = Fin D holds
b1 is with_countable_Cover
proof end;
end;

theorem :: SRINGS_2:6
for X being set holds Fin X is semiring_of_sets of X
proof end;

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:
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 ;

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
coherence
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:
proof end;

LL18:
proof end;

LL19:
proof end;

LL21:
proof end;

LL22:
proof end;

LL24:
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
coherence
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 end;