:: 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:] ) }

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 }

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

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 ;

for b_{1} being SigmaField of X holds

( b_{1} is cap-finite-partition-closed & b_{1} is diff-c=-finite-partition-closed & b_{1} is with_countable_Cover & b_{1} is with_empty_element )

end;
cluster non empty compl-closed sigma-multiplicative -> cap-finite-partition-closed diff-c=-finite-partition-closed with_countable_Cover with_empty_element for SigmaField of ;

coherence for b

( b

proof end;

theorem :: SRINGS_2:4

registration

let X be set ;

for b_{1} being Subset-Family of X st b_{1} = bool X holds

( b_{1} is cap-finite-partition-closed & b_{1} is diff-c=-finite-partition-closed & b_{1} is with_countable_Cover & not b_{1} is with_non-empty_elements )
;

end;
cluster K6(X) -> cap-finite-partition-closed diff-c=-finite-partition-closed with_countable_Cover with_empty_element for Subset-Family of X;

coherence for b

( b

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 ;

for b_{1} being Subset-Family of X st b_{1} = Fin X holds

( b_{1} is cap-finite-partition-closed & b_{1} is diff-c=-finite-partition-closed & not b_{1} is with_non-empty_elements )

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

coherence for b

( b

proof end;

registration

let D be denumerable set ;

coherence

for b_{1} being Subset-Family of D st b_{1} = Fin D holds

b_{1} is with_countable_Cover

end;
coherence

for b

b

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

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

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;

( 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 )

( S is cap-closed & S is diff-finite-partition-closed & S is with_empty_element & S is with_countable_Cover )

proof end;

definition

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

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},{}};

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

proof 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},{}};

sring4_8 = {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}};

set S = sring4_8 ;

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