:: Dynkin's Lemma in Measure Theory
:: by Franz Merkl
::
:: Received November 27, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, PROB_1, SUBSET_1, SETFAM_1, NUMBERS, RELAT_1, FUNCT_1,
FINSET_1, ARYTM_3, CARD_1, FUNCT_7, CARD_3, TARSKI, ZFMISC_1, PROB_2,
XXREAL_0, NAT_1, EQREL_1, DYNKIN, FINSUB_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, FINSET_1, CARD_1,
ORDINAL1, NUMBERS, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, XCMPLX_0, NAT_1,
FUNCT_7, CARD_3, PROB_1, FINSUB_1, PROB_2, XXREAL_0;
constructors SETFAM_1, FINSUB_1, NAT_1, PROB_2, XREAL_0, FUNCT_7, ENUMSET1,
RELSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FINSET_1,
XREAL_0, FUNCT_7, CARD_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities SUBSET_1, CARD_3, ORDINAL1;
expansions TARSKI;
theorems TARSKI, FUNCT_1, ZFMISC_1, FUNCT_2, SUBSET_1, NAT_1, RELAT_1,
SETFAM_1, PROB_2, FINSUB_1, XBOOLE_0, XBOOLE_1, PROB_1, ORDINAL1,
XXREAL_0, FUNCT_7, MEASURE1;
schemes FUNCT_2, NAT_1, FINSET_1, XFAMILY;
begin
reserve Omega, F for non empty set,
f for SetSequence of Omega,
X,A,B for Subset of Omega,
D for non empty Subset-Family of Omega,
n,m for Element of NAT,
h,x,y,z,u,v,Y,I for set;
:: Preliminaries ::
theorem Th1:
for f being SetSequence of Omega for x holds x in rng f iff ex n st f.n=x
proof
let f be SetSequence of Omega;
let x;
A1: now
assume x in rng f;
then consider z being object such that
A2: z in dom f and
A3: x=f.z by FUNCT_1:def 3;
reconsider n=z as Element of NAT by A2,FUNCT_2:def 1;
take n;
thus f.n=x by A3;
end;
dom f=NAT by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:def 3;
end;
Lm1: for X being non empty set for a,b,c being Element of X holds (a,b)
followed_by c is sequence of X;
definition
let Omega be non empty set;
let a,b,c be Subset of Omega;
redefine func (a,b) followed_by c -> SetSequence of Omega; :: redefines followed_by (FUNCT_7, definition)
coherence
proof
thus (a,b) followed_by c is SetSequence of Omega;
end;
end;
::$CT
theorem Th2:
for a,b being set holds Union (a,b) followed_by {} = a \/ b
proof
let a,b be set;
rng (a,b) followed_by {} = {a,b,{}} by FUNCT_7:127;
hence Union ((a,b) followed_by {}) = union{a,b} by MEASURE1:1
.= a \/ b by ZFMISC_1:75;
end;
definition
let Omega be non empty set;
let f be SetSequence of Omega;
let X be Subset of Omega;
func seqIntersection(X,f) -> SetSequence of Omega means
:Def1:
for n holds it.n = X /\ f.n;
existence
proof
deffunc F(Element of NAT) = X /\ f.$1;
consider g being sequence of bool Omega such that
A1: for x being Element of NAT holds g.x = F(x) from FUNCT_2:sch 4;
take g;
let n;
thus thesis by A1;
end;
uniqueness
proof
let i1,i2 be SetSequence of Omega;
assume
A2: for n holds i1.n=X/\ f.n;
assume
A3: for n holds i2.n=X/\ f.n;
now
let n be Element of NAT;
i1.n=X/\ f.n by A2;
hence i1.n=i2.n by A3;
end;
hence i1=i2 by FUNCT_2:63;
end;
end;
begin
:: disjoint-valued functions and intersection ::
definition
let Omega;
let f;
redefine attr f is disjoint_valued means :: redefines disjoint_valued (PROB_2, definition)
n<m implies f.n misses f.m;
compatibility
proof
thus f is disjoint_valued implies for n,m holds (n<m implies f.n misses f.
m) by PROB_2:def 2;
assume
A1: n<m implies f.n misses f.m;
now
let x,y be object;
assume
A2: x <> y;
per cases;
suppose
x in dom f & y in dom f;
then reconsider n = x, m = y as Element of NAT by FUNCT_2:def 1;
n < m or n > m by A2,XXREAL_0:1;
hence f.x misses f.y by A1;
end;
suppose
not (x in dom f & y in dom f);
then f.x = {} or f.y = {} by FUNCT_1:def 2;
hence f.x misses f.y by XBOOLE_1:65;
end;
end;
hence thesis by PROB_2:def 2;
end;
end;
theorem Th3:
for Y being non empty set holds for x holds x c= meet Y iff for y
being Element of Y holds x c= y
proof
let Y be non empty set;
let x;
thus x c= meet Y implies for y be Element of Y holds x c= y
by SETFAM_1:def 1;
assume
A1: for y being Element of Y holds x c= y;
let z be object;
assume
A2: z in x;
now
let u;
assume u in Y;
then x c= u by A1;
hence z in u by A2;
end;
hence thesis by SETFAM_1:def 1;
end;
notation
let x be set;
synonym x is intersection_stable for x is cap-closed;
end;
definition
let Omega be non empty set;
let f be SetSequence of Omega;
let n be Nat;
func disjointify(f,n) -> Subset of Omega equals
f.n \ union rng (f|n);
coherence;
end;
definition
let Omega be non empty set;
let g be SetSequence of Omega;
func disjointify(g) -> SetSequence of Omega means
:Def4:
for n being Nat holds it.n=disjointify(g,n);
existence
proof
deffunc F(Nat) = disjointify(g,$1);
consider f being sequence of bool Omega such that
A1: for x being Element of NAT holds f.x = F(x) from FUNCT_2:sch 4;
take f;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let i1,i2 be SetSequence of Omega;
assume
A2: for n be Nat holds i1.n=disjointify(g,n);
assume
A3: for n be Nat holds i2.n=disjointify(g,n);
now
let n be Element of NAT;
i1.n=disjointify(g,n) by A2;
hence i1.n=i2.n by A3;
end;
hence i1=i2 by FUNCT_2:63;
end;
end;
theorem Th4:
for n being Nat holds (disjointify(f)).n=f.n \ union rng(f|n)
proof
let n be Nat;
(disjointify f).n=disjointify(f,n) by Def4;
hence thesis;
end;
theorem Th5:
for f being SetSequence of Omega holds disjointify(f) is disjoint_valued
proof
let f be SetSequence of Omega;
now
let n,m;
assume n<m;
then
A1: n in Segm m by NAT_1:44;
dom f=NAT by FUNCT_2:def 1;
then dom(f|m)=m/\ NAT by RELAT_1:61;
then n in dom(f|m) by A1,XBOOLE_0:def 4;
then
A2: (f|m).n in rng(f|m) by FUNCT_1:def 3;
(f|m).n=f.n by A1,FUNCT_1:49;
then f.n misses f.m \ union rng(f|m) by A2,XBOOLE_1:85,ZFMISC_1:74;
then
A3: f.n misses (disjointify(f)).m by Th4;
f.n \ union rng(f|n) c= f.n by XBOOLE_1:36;
then (disjointify(f)).n c= f.n by Th4;
hence (disjointify(f)).n misses (disjointify(f)).m by A3,XBOOLE_1:63;
end;
hence thesis;
end;
theorem Th6:
for f being SetSequence of Omega holds union rng disjointify(f) = union rng f
proof
let f be SetSequence of Omega;
A1: dom f=NAT by FUNCT_2:def 1;
A2: dom disjointify f=NAT by FUNCT_2:def 1;
now
let x be object;
defpred P[Nat] means x in f.$1;
assume x in union rng f;
then consider y such that
A3: x in y and
A4: y in rng f by TARSKI:def 4;
consider z being object such that
A5: z in dom(f) and
A6: y=f.z by A4,FUNCT_1:def 3;
reconsider n=z as Element of NAT by A5,FUNCT_2:def 1;
A7: ex k being Nat st P[k]
proof
take n;
thus thesis by A3,A6;
end;
consider k being Nat such that
A8: P[k] & for m being Nat st P[m] holds k <= m from NAT_1:sch 5(A7);
now
assume x in union rng(f|k);
then consider y such that
A9: x in y and
A10: y in rng(f|k) by TARSKI:def 4;
consider z being object such that
A11: z in dom(f|k) and
A12: y=(f|k).z by A10,FUNCT_1:def 3;
dom(f|k) c= NAT by A1,RELAT_1:60;
then reconsider n=z as Element of NAT by A11;
dom(f|k) c= Segm k by RELAT_1:58;
then n<k & y=f.n by A11,A12,FUNCT_1:49,NAT_1:44;
hence contradiction by A8,A9;
end;
then x in f.k \ union rng(f|k) by A8,XBOOLE_0:def 5;
then
A13: x in (disjointify(f)).k by Th4;
k in NAT by ORDINAL1:def 12;
then (disjointify f).k in rng disjointify(f) by A2,FUNCT_1:def 3;
hence x in union rng disjointify(f) by A13,TARSKI:def 4;
end;
then
A14: union rng f c= union rng disjointify(f);
now
let x be object;
assume x in union rng disjointify(f);
then consider y such that
A15: x in y and
A16: y in rng disjointify(f) by TARSKI:def 4;
consider z being object such that
A17: z in dom(disjointify(f)) and
A18: y=(disjointify(f)).z by A16,FUNCT_1:def 3;
reconsider n=z as Element of NAT by A17,FUNCT_2:def 1;
A19: f.n\ union rng (f|n) c= f.n & f.n in rng(f) by A1,FUNCT_1:def 3
,XBOOLE_1:36;
x in f.n\ union rng (f|n) by A15,A18,Th4;
hence x in union rng f by A19,TARSKI:def 4;
end;
then union rng disjointify(f) c= union rng f;
hence thesis by A14,XBOOLE_0:def 10;
end;
theorem Th7:
for x,y being Subset of Omega st x misses y holds (x,y)
followed_by {} Omega is disjoint_valued
proof
let x,y be Subset of Omega such that
A1: x misses y;
reconsider r=(x,y) followed_by {} Omega as sequence of bool Omega;
now
let n,m;
A2: m>1 implies r.m={} by FUNCT_7:124;
assume
A3: n<m;
A4: now
assume
A5: m=0 or m=1;
0+1=1;
then n <= 0 by A3,A5,NAT_1:13;
hence n=0 & m=1 by A3,A5,NAT_1:3;
end;
r.0=x by FUNCT_7:122;
hence r.n misses r.m by A1,A4,A2,FUNCT_7:123,NAT_1:25,XBOOLE_1:65;
end;
hence thesis;
end;
theorem Th8:
for f being SetSequence of Omega holds f is disjoint_valued
implies for X being Subset of Omega holds seqIntersection(X,f) is
disjoint_valued
proof
let f be SetSequence of Omega;
assume
A1: f is disjoint_valued;
let X be Subset of Omega;
for n,m holds n<m implies (seqIntersection(X,f)).n misses (
seqIntersection(X,f)).m
proof
let n,m;
assume n<m;
then f.n misses f.m by A1;
then
A2: X/\ f.n misses f.m by XBOOLE_1:74;
(seqIntersection(X,f)).n=X/\ f.n & (seqIntersection(X,f)).m=X/\ f.m by Def1
;
hence thesis by A2,XBOOLE_1:74;
end;
hence thesis;
end;
theorem Th9:
for f being SetSequence of Omega for X being Subset of Omega
holds X/\ Union f= Union seqIntersection(X,f)
proof
let f be SetSequence of Omega;
let X be Subset of Omega;
A1: dom f=NAT by FUNCT_2:def 1;
now
reconsider g=seqIntersection(X,f) as SetSequence of Omega;
let z be object;
assume z in Union seqIntersection(X,f);
then consider u such that
A2: z in u and
A3: u in rng g by TARSKI:def 4;
consider v being object such that
A4: v in dom g and
A5: u=g.v by A3,FUNCT_1:def 3;
reconsider n=v as Element of NAT by A4,FUNCT_2:def 1;
A6: z in X/\ f.n by A2,A5,Def1;
then
A7: z in X by XBOOLE_0:def 4;
A8: f.n in rng f by A1,FUNCT_1:def 3;
z in f.n by A6,XBOOLE_0:def 4;
then z in Union f by A8,TARSKI:def 4;
hence z in X/\ Union f by A7,XBOOLE_0:def 4;
end;
then
A9: Union seqIntersection(X,f) c= X/\ Union f;
A10: dom seqIntersection(X,f)=NAT by FUNCT_2:def 1;
now
let z be object;
assume
A11: z in X/\ Union f;
then z in union rng f by XBOOLE_0:def 4;
then consider u such that
A12: z in u and
A13: u in rng f by TARSKI:def 4;
consider v being object such that
A14: v in dom f and
A15: u=f.v by A13,FUNCT_1:def 3;
reconsider n=v as Element of NAT by A14,FUNCT_2:def 1;
X/\ f.n = (seqIntersection(X,f)).n by Def1;
then
A16: X/\ f.n in rng seqIntersection(X,f) by A10,FUNCT_1:def 3;
z in X by A11,XBOOLE_0:def 4;
then z in X/\ f.n by A12,A15,XBOOLE_0:def 4;
hence z in Union seqIntersection(X,f) by A16,TARSKI:def 4;
end;
then X/\ Union f c= Union seqIntersection(X,f);
hence thesis by A9,XBOOLE_0:def 10;
end;
begin
:: Dynkin Systems:definition and closure properties ::
definition
let Omega;
mode Dynkin_System of Omega -> Subset-Family of Omega means
:Def5:
(for f
holds rng f c= it & f is disjoint_valued implies Union f in it) & (for X holds
X in it implies X` in it) & {} in it;
existence
proof
reconsider D = bool Omega as non empty Subset-Family of Omega;
take D;
{} c= Omega;
hence thesis;
end;
end;
registration
let Omega;
cluster -> non empty for Dynkin_System of Omega;
coherence by Def5;
end;
theorem Th10:
bool Omega is Dynkin_System of Omega
proof
A1: {} c= Omega & bool Omega c= bool Omega;
( for f holds rng f c= bool Omega & f is disjoint_valued implies Union f
in bool Omega)& for X holds X in bool Omega implies X`in bool Omega;
hence thesis by A1,Def5;
end;
theorem Th11:
(for Y st Y in F holds Y is Dynkin_System of Omega) implies meet
F is Dynkin_System of Omega
proof
assume
A1: for Y st Y in F holds Y is Dynkin_System of Omega;
now
let Y;
assume Y in F;
then Y is Dynkin_System of Omega by A1;
hence {} in Y by Def5;
end;
then
A2: {} in meet F by SETFAM_1:def 1;
A3: now
let f;
assume that
A4: rng f c= meet F and
A5: f is disjoint_valued;
now
let Y such that
A6: Y in F;
meet F c= Y by A6,SETFAM_1:3;
then
A7: rng f c= Y by A4;
Y is Dynkin_System of Omega by A1,A6;
hence Union f in Y by A5,A7,Def5;
end;
hence Union f in meet F by SETFAM_1:def 1;
end;
A8: now
let X;
assume
A9: X in meet F;
for Y st Y in F holds X` in Y
proof
let Y;
assume Y in F;
then Y is Dynkin_System of Omega & meet F c= Y by A1,SETFAM_1:3;
hence thesis by A9,Def5;
end;
hence X` in meet F by SETFAM_1:def 1;
end;
set Y = the Element of F;
A10: meet F c= Y by SETFAM_1:3;
Y is Dynkin_System of Omega by A1;
then meet F is Subset-Family of Omega by A10,XBOOLE_1:1;
hence thesis by A3,A8,A2,Def5;
end;
theorem Th12:
D is Dynkin_System of Omega & D is intersection_stable implies (
A in D & B in D implies A\B in D)
proof
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable;
assume that
A3: A in D and
A4: B in D;
B`in D by A1,A4,Def5;
then A /\ (B`) in D by A2,A3,FINSUB_1:def 2;
hence thesis by SUBSET_1:13;
end;
theorem Th13:
D is Dynkin_System of Omega & D is intersection_stable implies (
A in D & B in D implies A \/ B in D)
proof
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable;
assume A in D & B in D;
then A`in D & B`in D by A1,Def5;
then A`/\ B`in D by A2,FINSUB_1:def 2;
then (A \/ B)`in D by XBOOLE_1:53;
then (A \/ B)``in D by A1,Def5;
hence thesis;
end;
theorem Th14:
D is Dynkin_System of Omega & D is intersection_stable implies
for x being finite set holds x c= D implies union x in D
proof
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable;
defpred P[set] means union $1 in D;
let x be finite set;
assume
A3: x c= D;
A4: for y,b being set st y in x & b c= x & P[b] holds P[b \/ {y}]
proof
let y,b be set such that
A5: y in x and
b c= x and
A6: union b in D;
y in D by A3,A5;
then reconsider y1=y as Subset of Omega;
reconsider unionb = union b as Subset of Omega by A6;
union {y}=y & unionb \/ y1 in D by A1,A2,A3,A5,A6,Th13,ZFMISC_1:25;
hence thesis by ZFMISC_1:78;
end;
A7: x is finite;
A8: P[{}] by A1,Def5,ZFMISC_1:2;
thus P[x] from FINSET_1:sch 2(A7,A8,A4);
end;
theorem Th15:
D is Dynkin_System of Omega & D is intersection_stable implies
for f being SetSequence of Omega holds rng f c= D implies rng disjointify(f) c=
D
proof
assume
A1: D is Dynkin_System of Omega & D is intersection_stable;
let f be SetSequence of Omega;
assume
A2: rng f c= D;
A3: for n holds (disjointify(f)).n in D
proof
let n;
A4: rng (f|n) c= rng(f) by RELAT_1:70;
A5: union rng(f|n)in D by A1,A2,A4,Th14,XBOOLE_1:1;
then reconsider urf=union rng(f|n) as Subset of Omega;
dom(f)=NAT by FUNCT_2:def 1;
then f.n in rng f by FUNCT_1:def 3;
then f.n \ urf in D by A1,A2,A5,Th12;
hence thesis by Th4;
end;
let y be object;
assume y in rng disjointify(f);
then consider x being object such that
A6: x in dom(disjointify(f)) and
A7: y=(disjointify(f)).x by FUNCT_1:def 3;
reconsider n=x as Element of NAT by A6,FUNCT_2:def 1;
y=(disjointify(f)).n by A7;
hence y in D by A3;
end;
theorem Th16:
D is Dynkin_System of Omega & D is intersection_stable implies
for f being SetSequence of Omega holds rng f c= D implies union rng f in D
proof
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable;
let f be SetSequence of Omega;
assume rng f c= D;
then
A3: rng disjointify(f) c= D by A1,A2,Th15;
disjointify(f) is disjoint_valued by Th5;
then Union disjointify(f) in D by A1,A3,Def5;
hence thesis by Th6;
end;
theorem Th17:
for D being Dynkin_System of Omega for x,y being Element of D
holds x misses y implies x \/ y in D
proof
let D be Dynkin_System of Omega;
reconsider e={} as Element of D by Def5;
let x,y be Element of D;
reconsider x1=x as Subset of Omega;
reconsider y1=y as Subset of Omega;
reconsider r= (x1,y1) followed_by {} Omega as SetSequence of Omega;
(x,y) followed_by e is sequence of D by Lm1;
then
A1: rng r c= D by RELAT_1:def 19;
assume x misses y;
then r is disjoint_valued by Th7;
then Union r in D by A1,Def5;
hence thesis by Th2;
end;
theorem Th18:
for D being Dynkin_System of Omega for x,y being Element of D
holds x c= y implies y\x in D
proof
let D be Dynkin_System of Omega;
let x,y be Element of D;
A1: (x \/ y`)` = x` /\ y`` by XBOOLE_1:53
.= y\x by SUBSET_1:13;
assume x c= y;
then x c= y``;
then
A2: x misses y` by SUBSET_1:23;
y`in D by Def5;
then x \/ y` in D by A2,Th17;
hence thesis by A1,Def5;
end;
begin
:: Main steps for Dynkin's Lemma ::
theorem Th19:
D is Dynkin_System of Omega & D is intersection_stable implies D
is SigmaField of Omega
proof
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable;
A3: for f st rng f c= D holds Intersection f in D
proof
let f such that
A4: rng f c= D;
A5: for n holds (f.n)`in D
proof
let n;
f.n in rng f by NAT_1:51;
hence thesis by A1,A4,Def5;
end;
A6: for n holds (Complement f).n in D
proof
let n;
(Complement f).n=(f.n)` by PROB_1:def 2;
hence thesis by A5;
end;
for x being object st x in rng Complement f holds x in D
proof
let x be object;
assume x in rng Complement f;
then consider z being object such that
A7: z in dom Complement f and
A8: x=(Complement f).z by FUNCT_1:def 3;
reconsider n=z as Element of NAT by A7,FUNCT_2:def 1;
x=(Complement f).n by A8;
hence thesis by A6;
end;
then rng Complement f c= D;
then Union Complement f in D by A1,A2,Th16;
then (Union Complement f)` in D by A1,Def5;
hence thesis by PROB_1:def 3;
end;
for X st X in D holds X`in D by A1,Def5;
hence thesis by A3,PROB_1:15;
end;
definition
let Omega be non empty set;
let E be Subset-Family of Omega;
func generated_Dynkin_System(E) -> Dynkin_System of Omega means
:Def6:
E c= it & for D being Dynkin_System of Omega holds (E c= D implies it c= D);
existence
proof
defpred P[set] means $1 is Dynkin_System of Omega & E c= $1;
consider Y such that
A1: for x holds x in Y iff x in bool bool Omega & P[x]
from XFAMILY:sch 1;
bool Omega is Dynkin_System of Omega by Th10;
then reconsider Y as non empty set by A1;
for z st z in Y holds z is Dynkin_System of Omega by A1;
then reconsider I=meet Y as Dynkin_System of Omega by Th11;
take I;
for y being Element of Y holds E c= y by A1;
hence E c= I by Th3;
let D be Dynkin_System of Omega;
assume E c= D;
then D in Y by A1;
hence thesis by SETFAM_1:3;
end;
uniqueness
proof
let I1,I2 be Dynkin_System of Omega;
assume
A2: E c= I1 & for D being Dynkin_System of Omega holds (E c= D implies
I1 c= D);
assume E c= I2 & for D being Dynkin_System of Omega holds (E c= D implies
I2 c= D);
then I1 c= I2 & I2 c= I1 by A2;
hence thesis by XBOOLE_0:def 10;
end;
end;
definition
let Omega be non empty set;
let G be set;
let X be Subset of Omega;
func DynSys(X,G) -> Subset-Family of Omega means
:Def7:
for A being Subset of Omega holds A in it iff A /\ X in G;
existence
proof
defpred P[set] means $1 /\ X in G;
consider I such that
A1: for x holds x in I iff x in bool Omega & P[x] from XFAMILY:sch 1;
for x being object holds x in I implies x in bool Omega by A1;
then reconsider I as Subset-Family of Omega by TARSKI:def 3;
take I;
let A be Subset of Omega;
thus thesis by A1;
end;
uniqueness
proof
let I1,I2 be Subset-Family of Omega;
assume
A2: for A being Subset of Omega holds A in I1 iff A /\ X in G;
assume
A3: for A being Subset of Omega holds A in I2 iff A/\ X in G;
now
let A be Subset of Omega;
A in I1 iff A /\ X in G by A2;
hence A in I1 iff A in I2 by A3;
end;
hence thesis by SUBSET_1:3;
end;
end;
definition
let Omega be non empty set;
let G be Dynkin_System of Omega;
let X be Element of G;
redefine func DynSys(X,G) -> Dynkin_System of Omega; :: redefines DynSys (DYNKIN, definition)
coherence
proof
A1: for f being SetSequence of Omega holds rng f c= DynSys(X,G) & f is
disjoint_valued implies Union f in DynSys(X,G)
proof
reconsider X1=X as Subset of Omega;
let f be SetSequence of Omega;
assume that
A2: rng f c= DynSys(X,G) and
A3: f is disjoint_valued;
now
let x be object;
assume x in rng seqIntersection(X1,f);
then consider n such that
A4: x=(seqIntersection(X1,f)).n by Th1;
A5: f.n in rng f by Th1;
x=X/\ f.n by A4,Def1;
hence x in G by A2,A5,Def7;
end;
then
A6: rng seqIntersection(X1,f) c= G;
seqIntersection(X,f) is disjoint_valued by A3,Th8;
then Union seqIntersection(X1,f) in G by A6,Def5;
then X/\ Union f in G by Th9;
hence thesis by Def7;
end;
A7: for A being Subset of Omega holds A in DynSys(X,G) implies A` in
DynSys(X,G)
proof
let A be Subset of Omega;
X misses X` by XBOOLE_1:79;
then
A8: X /\ X` = {} by XBOOLE_0:def 7;
assume A in DynSys(X,G);
then X /\ A in G by Def7;
then
A9: X\(X/\ A)in G by Th18,XBOOLE_1:17;
X\(X/\ A) = X /\ (X/\ A)` by SUBSET_1:13
.= X /\ (X` \/ A`) by XBOOLE_1:54
.= (X/\ X`) \/ (X/\ A`) by XBOOLE_1:23
.= X/\ A` by A8;
hence thesis by A9,Def7;
end;
{}/\ X={} & {}in G by Def5;
then {}in DynSys(X,G) by Def7;
hence thesis by A1,A7,Def5;
end;
end;
theorem Th20:
for E being Subset-Family of Omega for X,Y being Subset of Omega
holds X in E & Y in generated_Dynkin_System(E) & E is intersection_stable
implies X/\ Y in generated_Dynkin_System(E)
proof
let E be Subset-Family of Omega;
let X,Y be Subset of Omega;
assume that
A1: X in E and
A2: Y in generated_Dynkin_System(E) and
A3: E is intersection_stable;
reconsider G=generated_Dynkin_System(E) as Dynkin_System of Omega;
E c= generated_Dynkin_System(E) by Def6;
then reconsider X as Element of G by A1;
for x being object holds x in E implies x in DynSys(X,G)
proof
let x be object;
assume
A4: x in E;
then reconsider x as Subset of Omega;
A5: E c= G by Def6;
x /\ X in E by A1,A3,A4,FINSUB_1:def 2;
hence thesis by A5,Def7;
end;
then E c= DynSys(X,G);
then generated_Dynkin_System(E) c= DynSys(X,G) by Def6;
hence thesis by A2,Def7;
end;
theorem Th21:
for E being Subset-Family of Omega for X,Y being Subset of Omega
holds X in generated_Dynkin_System(E) & Y in generated_Dynkin_System(E) & E is
intersection_stable implies X/\ Y in generated_Dynkin_System(E)
proof
let E be Subset-Family of Omega;
let X,Y be Subset of Omega;
assume that
A1: X in generated_Dynkin_System(E) and
A2: Y in generated_Dynkin_System(E) and
A3: E is intersection_stable;
reconsider G=generated_Dynkin_System(E) as Dynkin_System of Omega;
defpred P[set] means ex X being Element of G st $1=DynSys(X,G);
consider h such that
A4: for x holds x in h iff x in bool bool Omega & P[x] from XFAMILY:sch
1;
A5: for Y st Y in h holds Y is Dynkin_System of Omega
proof
let Y;
assume Y in h;
then ex X being Element of G st Y=DynSys(X,G) by A4;
hence thesis;
end;
h is non empty
proof
set X = the Element of G;
DynSys(X,G) in h by A4;
hence thesis;
end;
then reconsider h as non empty set;
DynSys(X,G)in h by A1,A4;
then
A6: meet h c= DynSys(X,G) by SETFAM_1:3;
for x being object holds x in E implies x in meet h
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A7: x in E;
for Y st Y in h holds x in Y
proof
let Y;
assume Y in h;
then consider X being Element of G such that
A8: Y=DynSys(X,G) by A4;
xx/\ X in G by A3,A7,Th20;
hence thesis by A7,A8,Def7;
end;
hence thesis by SETFAM_1:def 1;
end;
then
A9: E c= meet h;
meet h is Dynkin_System of Omega by A5,Th11;
then G c= meet h by A9,Def6;
then G c= DynSys(X,G) by A6;
hence thesis by A2,Def7;
end;
theorem Th22:
for E being Subset-Family of Omega st E is intersection_stable
holds generated_Dynkin_System(E) is intersection_stable
proof
let E be Subset-Family of Omega such that
A1: E is intersection_stable;
reconsider G=generated_Dynkin_System(E) as Subset-Family of Omega;
for a,b being set st a in G & b in G holds a/\ b in G by A1,Th21;
hence thesis by FINSUB_1:def 2;
end;
::$N Dynkin Lemma
theorem
for E being Subset-Family of Omega st E is intersection_stable for D
being Dynkin_System of Omega st E c= D holds sigma(E) c= D
proof
let E be Subset-Family of Omega such that
A1: E is intersection_stable;
reconsider G=generated_Dynkin_System(E) as Dynkin_System of Omega;
G is intersection_stable by A1,Th22;
then
A2: G is SigmaField of Omega by Th19;
let D be Dynkin_System of Omega;
assume E c= D;
then
A3: G c= D by Def6;
E c= G by Def6;
then sigma(E) c= G by A2,PROB_1:def 9;
hence thesis by A3;
end;