:: by Noboru Endou , Kazuhisa Nakasho and Yasunari Shidama

::

:: Received February 18, 2015

:: Copyright (c) 2015-2019 Association of Mizar Users

theorem Lem10: :: SRINGS_3:1

for f1, f2 being FinSequence

for k being Nat st k in Seg ((len f1) * (len f2)) holds

( ((k -' 1) mod (len f2)) + 1 in dom f2 & ((k -' 1) div (len f2)) + 1 in dom f1 )

for k being Nat st k in Seg ((len f1) * (len f2)) holds

( ((k -' 1) mod (len f2)) + 1 in dom f2 & ((k -' 1) div (len f2)) + 1 in dom f1 )

proof end;

theorem TT1: :: SRINGS_3:5

for f1, f2 being FinSequence ex f being FinSequence st

( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds

f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) )

( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds

f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) )

proof end;

theorem TT2: :: SRINGS_3:6

for f1, f2 being disjoint_valued FinSequence ex f being disjoint_valued FinSequence st

( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds

f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) )

( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds

f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) )

proof end;

registration

let X be set ;

coherence

for b_{1} being Subset-Family of X st not b_{1} is empty & b_{1} is diff-closed holds

b_{1} is with_empty_element

end;
coherence

for b

b

proof end;

definition

let IT be set ;

end;
attr IT is semi-diff-closed means :DefSD: :: SRINGS_3:def 1

for X, Y being set st X in IT & Y in IT holds

ex F being disjoint_valued FinSequence of IT st X \ Y = Union F;

for X, Y being set st X in IT & Y in IT holds

ex F being disjoint_valued FinSequence of IT st X \ Y = Union F;

:: deftheorem DefSD defines semi-diff-closed SRINGS_3:def 1 :

for IT being set holds

( IT is semi-diff-closed iff for X, Y being set st X in IT & Y in IT holds

ex F being disjoint_valued FinSequence of IT st X \ Y = Union F );

for IT being set holds

( IT is semi-diff-closed iff for X, Y being set st X in IT & Y in IT holds

ex F being disjoint_valued FinSequence of IT st X \ Y = Union F );

TV1: for X being set holds bool X is semi-diff-closed

proof end;

registration
end;

registration

let X be set ;

existence

ex b_{1} being Subset-Family of X st

( not b_{1} is empty & b_{1} is semi-diff-closed & b_{1} is cap-closed )

end;
existence

ex b

( not b

proof end;

:: Following cluster gives classical definition of a semiring of sets

registration

let X be set ;

existence

ex b_{1} being Subset-Family of X st

( b_{1} is with_empty_element & b_{1} is semi-diff-closed & b_{1} is cap-closed )

end;
existence

ex b

( b

proof end;

definition

let X be set ;

mode Semiring of X is with_empty_element cap-closed semi-diff-closed Subset-Family of X;

end;
mode Semiring of X is with_empty_element cap-closed semi-diff-closed Subset-Family of X;

theorem Lm1: :: SRINGS_3:8

for X being set

for S being Subset-Family of X

for S1, S2 being set st S1 in S & S2 in S & S is semi-diff-closed holds

ex x being finite Subset of S st x is a_partition of S1 \ S2

for S being Subset-Family of X

for S1, S2 being set st S1 in S & S2 in S & S is semi-diff-closed holds

ex x being finite Subset of S st x is a_partition of S1 \ S2

proof end;

theorem :: SRINGS_3:9

for X being set

for S being non empty Subset-Family of X st S is semi-diff-closed holds

S is diff-c=-finite-partition-closed

for S being non empty Subset-Family of X st S is semi-diff-closed holds

S is diff-c=-finite-partition-closed

proof end;

theorem th10: :: SRINGS_3:10

for X being set

for S being Subset-Family of X st S is with_empty_element & S is cap-finite-partition-closed & S is diff-c=-finite-partition-closed holds

S is semi-diff-closed

for S being Subset-Family of X st S is with_empty_element & S is cap-finite-partition-closed & S is diff-c=-finite-partition-closed holds

S is semi-diff-closed

proof end;

registration

correctness

coherence

for b_{1} being set st b_{1} is diff-closed holds

( b_{1} is semi-diff-closed & b_{1} is cap-closed );

end;
coherence

for b

( b

proof end;

registration

let X be set ;

existence

ex b_{1} being Subset-Family of X st

( not b_{1} is empty & b_{1} is preBoolean )

end;
existence

ex b

( not b

proof end;

registration

correctness

coherence

for b_{1} being set st not b_{1} is empty & b_{1} is preBoolean holds

b_{1} is with_empty_element ;

end;
coherence

for b

b

proof end;

ExistRing: for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X ex Y being non empty preBoolean Subset-Family of X st Y = meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z }

proof end;

definition

let X be set ;

let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X;

coherence

meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } is non empty preBoolean Subset-Family of X;

end;
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X;

func Ring_generated_by S -> non empty preBoolean Subset-Family of X equals :: SRINGS_3:def 2

meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ;

correctness meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ;

coherence

meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } is non empty preBoolean Subset-Family of X;

proof end;

:: deftheorem defines Ring_generated_by SRINGS_3:def 2 :

for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds Ring_generated_by S = meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ;

for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds Ring_generated_by S = meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ;

theorem RingGen1: :: SRINGS_3:11

for X being set

for P being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds P c= Ring_generated_by P

for P being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds P c= Ring_generated_by P

proof end;

lemma100: for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X

for P being set st P = { A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } holds

( P is non empty Subset-Family of X & S c= P )

proof end;

definition

let X be set ;

let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X;

{ A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } is non empty Subset-Family of X by lemma100;

end;
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X;

func DisUnion S -> non empty Subset-Family of X equals :: SRINGS_3:def 3

{ A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } ;

coherence { A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } ;

{ A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } is non empty Subset-Family of X by lemma100;

:: deftheorem defines DisUnion SRINGS_3:def 3 :

for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds DisUnion S = { A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } ;

for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds DisUnion S = { A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } ;

theorem :: SRINGS_3:12

for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds S c= DisUnion S by lemma100;

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds S c= DisUnion S by lemma100;

theorem lemma101: :: SRINGS_3:13

for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds DisUnion S is cap-closed

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds DisUnion S is cap-closed

proof end;

theorem lemma102: :: SRINGS_3:14

for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X

for A, B, P being set st P = DisUnion S & A in P & B in P & A misses B holds

A \/ B in P

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X

for A, B, P being set st P = DisUnion S & A in P & B in P & A misses B holds

A \/ B in P

proof end;

theorem lemma103: :: SRINGS_3:15

for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X

for A, B being set st A in S & B in S holds

B \ A in DisUnion S

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X

for A, B being set st A in S & B in S holds

B \ A in DisUnion S

proof end;

theorem lemma104: :: SRINGS_3:16

for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X

for A, B being set st A in S & B in DisUnion S holds

B \ A in DisUnion S

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X

for A, B being set st A in S & B in DisUnion S holds

B \ A in DisUnion S

proof end;

theorem lemma105: :: SRINGS_3:17

for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X

for A, B, R being set st R = DisUnion S & A in R & B in R & A <> {} holds

B \ A in R

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X

for A, B, R being set st R = DisUnion S & A in R & B in R & A <> {} holds

B \ A in R

proof end;

theorem :: SRINGS_3:18

for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds Ring_generated_by S = DisUnion S

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds Ring_generated_by S = DisUnion S

proof end;

definition

let X be set ;

ex b_{1} being non empty preBoolean Subset-Family of X st

for F being SetSequence of X st rng F c= b_{1} holds

Union F in b_{1}

end;
mode SigmaRing of X -> non empty preBoolean Subset-Family of X means :DefSigmaRing: :: SRINGS_3:def 4

for F being SetSequence of X st rng F c= it holds

Union F in it;

existence for F being SetSequence of X st rng F c= it holds

Union F in it;

ex b

for F being SetSequence of X st rng F c= b

Union F in b

proof end;

:: deftheorem DefSigmaRing defines SigmaRing SRINGS_3:def 4 :

for X being set

for b_{2} being non empty preBoolean Subset-Family of X holds

( b_{2} is SigmaRing of X iff for F being SetSequence of X st rng F c= b_{2} holds

Union F in b_{2} );

for X being set

for b

( b

Union F in b

LemX: for X being set

for S being SigmaRing of X holds S is sigma-multiplicative

proof end;

registration

let X be set ;

coherence

for b_{1} being SigmaRing of X holds b_{1} is sigma-multiplicative
by LemX;

end;
coherence

for b

definition

let X be set ;

let S be Subset-Family of X;

ex b_{1} being SigmaRing of X st

( S c= b_{1} & ( for Z being set st S c= Z & Z is SigmaRing of X holds

b_{1} c= Z ) )

uniqueness

for b_{1}, b_{2} being SigmaRing of X st S c= b_{1} & ( for Z being set st S c= Z & Z is SigmaRing of X holds

b_{1} c= Z ) & S c= b_{2} & ( for Z being set st S c= Z & Z is SigmaRing of X holds

b_{2} c= Z ) holds

b_{1} = b_{2};

;

end;
let S be Subset-Family of X;

func sigmaring S -> SigmaRing of X means :Defsigmaring: :: SRINGS_3:def 5

( S c= it & ( for Z being set st S c= Z & Z is SigmaRing of X holds

it c= Z ) );

existence ( S c= it & ( for Z being set st S c= Z & Z is SigmaRing of X holds

it c= Z ) );

ex b

( S c= b

b

proof end;

correctness uniqueness

for b

b

b

b

;

:: deftheorem Defsigmaring defines sigmaring SRINGS_3:def 5 :

for X being set

for S being Subset-Family of X

for b_{3} being SigmaRing of X holds

( b_{3} = sigmaring S iff ( S c= b_{3} & ( for Z being set st S c= Z & Z is SigmaRing of X holds

b_{3} c= Z ) ) );

for X being set

for S being Subset-Family of X

for b

( b

b

theorem :: SRINGS_3:19

for X being set

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds sigmaring (Ring_generated_by S) = sigmaring S

for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds sigmaring (Ring_generated_by S) = sigmaring S

proof end;

definition

let X be set ;

ex b_{1} being with_empty_element cap-closed semi-diff-closed Subset-Family of X st X in b_{1}

end;
mode semialgebra_of_sets of X -> with_empty_element cap-closed semi-diff-closed Subset-Family of X means :Def1: :: SRINGS_3:def 6

X in it;

existence X in it;

ex b

proof end;

:: deftheorem Def1 defines semialgebra_of_sets SRINGS_3:def 6 :

for X being set

for b_{2} being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds

( b_{2} is semialgebra_of_sets of X iff X in b_{2} );

for X being set

for b

( b

theorem :: SRINGS_3:20

for X being set

for F being Field_Subset of X holds F is semialgebra_of_sets of X by Def1, PROB_1:5;

for F being Field_Subset of X holds F is semialgebra_of_sets of X by Def1, PROB_1:5;

ExistAlgebra: for X being set

for S being semialgebra_of_sets of X ex Y being Field_Subset of X st Y = meet { Z where Z is Field_Subset of X : S c= Z }

proof end;

definition

let X be set ;

let S be semialgebra_of_sets of X;

coherence

meet { Z where Z is Field_Subset of X : S c= Z } is Field_Subset of X;

end;
let S be semialgebra_of_sets of X;

func Field_generated_by S -> Field_Subset of X equals :: SRINGS_3:def 7

meet { Z where Z is Field_Subset of X : S c= Z } ;

correctness meet { Z where Z is Field_Subset of X : S c= Z } ;

coherence

meet { Z where Z is Field_Subset of X : S c= Z } is Field_Subset of X;

proof end;

:: deftheorem defines Field_generated_by SRINGS_3:def 7 :

for X being set

for S being semialgebra_of_sets of X holds Field_generated_by S = meet { Z where Z is Field_Subset of X : S c= Z } ;

for X being set

for S being semialgebra_of_sets of X holds Field_generated_by S = meet { Z where Z is Field_Subset of X : S c= Z } ;

theorem :: SRINGS_3:23

for X being non empty set

for S being semialgebra_of_sets of X holds sigma (Field_generated_by S) = sigma S

for S being semialgebra_of_sets of X holds sigma (Field_generated_by S) = sigma S

proof end;

theorem :: SRINGS_3:26

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

( S is with_empty_element & S is semi-diff-closed & S is cap-closed )

( S is with_empty_element & S is semi-diff-closed & S is cap-closed )

proof end;

INTERVAL01: for I being Subset of REAL st I = {} holds

I is right_open_interval

proof end;

INTERVAL02: for I, J being Subset of REAL st I is right_open_interval & J is right_open_interval & I meets J holds

ex K, L being Subset of REAL st

( K is right_open_interval & L is right_open_interval & K misses L & I \ J = K \/ L )

proof end;

OOdif: for I, J being Subset of REAL st I is open_interval & J is open_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

COdif: for I, J being Subset of REAL st I is closed_interval & J is open_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

ROdif: for I, J being Subset of REAL st I is right_open_interval & J is open_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

LOdif: for I, J being Subset of REAL st I is left_open_interval & J is open_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

OCdif: for I, J being Subset of REAL st I is open_interval & J is closed_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

CCdif: for I, J being Subset of REAL st I is closed_interval & J is closed_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

RCdif: for I, J being Subset of REAL st I is right_open_interval & J is closed_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

LCdif: for I, J being Subset of REAL st I is left_open_interval & J is closed_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

ORdif: for I, J being Subset of REAL st I is open_interval & J is right_open_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

CRdif: for I, J being Subset of REAL st I is closed_interval & J is right_open_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

RRdif: for I, J being Subset of REAL st I is right_open_interval & J is right_open_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

LRdif: for I, J being Subset of REAL st I is left_open_interval & J is right_open_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

OLdif: for I, J being Subset of REAL st I is open_interval & J is left_open_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

CLdif: for I, J being Subset of REAL st I is closed_interval & J is left_open_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

RLdif: for I, J being Subset of REAL st I is right_open_interval & J is left_open_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

LLdif: for I, J being Subset of REAL st I is left_open_interval & J is left_open_interval & I meets J holds

ex K, L being Interval st

( K misses L & I \ J = K \/ L )

proof end;

INTERVAL03: for I, J being Subset of REAL st I is right_open_interval & J is right_open_interval holds

I /\ J is right_open_interval

proof end;

OOmeet: for I, J being Interval st I is open_interval & J is open_interval & I meets J holds

I /\ J is Interval

proof end;

OCmeet: for I, J being Interval st I is open_interval & J is closed_interval & I meets J holds

I /\ J is Interval

proof end;

ORmeet: for I, J being Interval st I is open_interval & J is right_open_interval & I meets J holds

I /\ J is Interval

proof end;

OLmeet: for I, J being Interval st I is open_interval & J is left_open_interval & I meets J holds

I /\ J is Interval

proof end;

CCmeet: for I, J being Interval st I is closed_interval & J is closed_interval & I meets J holds

I /\ J is Interval

proof end;

CRmeet: for I, J being Interval st I is closed_interval & J is right_open_interval & I meets J holds

I /\ J is Interval

proof end;

CLmeet: for I, J being Interval st I is closed_interval & J is left_open_interval & I meets J holds

I /\ J is Interval

proof end;

RRmeet: for I, J being Interval st I is right_open_interval & J is right_open_interval & I meets J holds

I /\ J is Interval

proof end;

RLmeet: for I, J being Interval st I is right_open_interval & J is left_open_interval & I meets J holds

I /\ J is Interval

proof end;

LLmeet: for I, J being Interval st I is left_open_interval & J is left_open_interval & I meets J holds

I /\ J is Interval

proof end;

theorem :: SRINGS_3:27

for S being Subset-Family of REAL st S = { I where I is Subset of REAL : I is right_open_interval } holds

( S is with_empty_element & S is semi-diff-closed & S is cap-closed )

( S is with_empty_element & S is semi-diff-closed & S is cap-closed )

proof end;