:: DYNKIN semantic presentation
begin
theorem Th1: :: DYNKIN:1
for Omega being non empty set
for f being SetSequence of Omega
for x being set holds
( x in rng f iff ex n being Element of NAT st f . n = x )
proof
let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega
for x being set holds
( x in rng f iff ex n being Element of NAT st f . n = x )
let f be SetSequence of Omega; ::_thesis: for x being set holds
( x in rng f iff ex n being Element of NAT st f . n = x )
let x be set ; ::_thesis: ( x in rng f iff ex n being Element of NAT st f . n = x )
A1: now__::_thesis:_(_x_in_rng_f_implies_ex_n_being_Element_of_NAT_st_f_._n_=_x_)
assume x in rng f ; ::_thesis: ex n being Element of NAT st f . n = x
then consider z being set 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 = n; ::_thesis: f . n = x
thus f . n = x by A3; ::_thesis: verum
end;
dom f = NAT by FUNCT_2:def_1;
hence ( x in rng f iff ex n being Element of NAT st f . n = x ) by A1, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th2: :: DYNKIN:2
for n being Element of NAT holds n is finite
proof
defpred S1[ Element of NAT ] means $1 is finite ;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then succ n is finite ;
hence S1[n + 1] by NAT_1:38; ::_thesis: verum
end;
A2: S1[ 0 ] ;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1); ::_thesis: verum
end;
registration
let n be Element of NAT ;
cluster Segm n -> finite ;
coherence
Segm n is finite by Th2;
end;
Lm1: for X being non empty set
for a, b, c being Element of X holds (a,b) followed_by c is Function of NAT,X
;
definition
let Omega be non empty set ;
let a, b, c be Subset of Omega;
:: original: followed_by
redefine func(a,b) followed_by c -> SetSequence of Omega;
coherence
(a,b) followed_by c is SetSequence of Omega
proof
thus (a,b) followed_by c is SetSequence of Omega ; ::_thesis: verum
end;
end;
theorem Th3: :: DYNKIN:3
for a, b being set holds Union ((a,b) followed_by {}) = a \/ b
proof
let a, b be set ; ::_thesis: Union ((a,b) followed_by {}) = a \/ b
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 ;
::_thesis: verum
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: :: DYNKIN:def 1
for n being Element of NAT holds it . n = X /\ (f . n);
existence
ex b1 being SetSequence of Omega st
for n being Element of NAT holds b1 . n = X /\ (f . n)
proof
deffunc H1( Element of NAT ) -> Element of bool Omega = X /\ (f . $1);
consider g being Function of NAT,(bool Omega) such that
A1: for x being Element of NAT holds g . x = H1(x) from FUNCT_2:sch_4();
take g ; ::_thesis: for n being Element of NAT holds g . n = X /\ (f . n)
let n be Element of NAT ; ::_thesis: g . n = X /\ (f . n)
thus g . n = X /\ (f . n) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being SetSequence of Omega st ( for n being Element of NAT holds b1 . n = X /\ (f . n) ) & ( for n being Element of NAT holds b2 . n = X /\ (f . n) ) holds
b1 = b2
proof
let i1, i2 be SetSequence of Omega; ::_thesis: ( ( for n being Element of NAT holds i1 . n = X /\ (f . n) ) & ( for n being Element of NAT holds i2 . n = X /\ (f . n) ) implies i1 = i2 )
assume A2: for n being Element of NAT holds i1 . n = X /\ (f . n) ; ::_thesis: ( ex n being Element of NAT st not i2 . n = X /\ (f . n) or i1 = i2 )
assume A3: for n being Element of NAT holds i2 . n = X /\ (f . n) ; ::_thesis: i1 = i2
now__::_thesis:_for_n_being_Element_of_NAT_holds_i1_._n_=_i2_._n
let n be Element of NAT ; ::_thesis: i1 . n = i2 . n
i1 . n = X /\ (f . n) by A2;
hence i1 . n = i2 . n by A3; ::_thesis: verum
end;
hence i1 = i2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines seqIntersection DYNKIN:def_1_:_
for Omega being non empty set
for f being SetSequence of Omega
for X being Subset of Omega
for b4 being SetSequence of Omega holds
( b4 = seqIntersection (X,f) iff for n being Element of NAT holds b4 . n = X /\ (f . n) );
begin
definition
let Omega be non empty set ;
let f be SetSequence of Omega;
:: original: disjoint_valued
redefine attrf is disjoint_valued means :Def2: :: DYNKIN:def 2
for n, m being Element of NAT st n < m holds
f . n misses f . m;
compatibility
( f is disjoint_valued iff for n, m being Element of NAT st n < m holds
f . n misses f . m )
proof
thus ( f is disjoint_valued implies for n, m being Element of NAT st n < m holds
f . n misses f . m ) by PROB_2:def_2; ::_thesis: ( ( for n, m being Element of NAT st n < m holds
f . n misses f . m ) implies f is disjoint_valued )
assume A1: for n, m being Element of NAT st n < m holds
f . n misses f . m ; ::_thesis: f is disjoint_valued
now__::_thesis:_for_x,_y_being_set_st_x_<>_y_holds_
f_._x_misses_f_._y
let x, y be set ; ::_thesis: ( x <> y implies f . b1 misses f . b2 )
assume A2: x <> y ; ::_thesis: f . b1 misses f . b2
percases ( ( x in dom f & y in dom f ) or not x in dom f or not y in dom f ) ;
suppose ( x in dom f & y in dom f ) ; ::_thesis: f . b1 misses f . b2
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; ::_thesis: verum
end;
suppose ( not x in dom f or not y in dom f ) ; ::_thesis: f . b1 misses f . b2
then ( f . x = {} or f . y = {} ) by FUNCT_1:def_2;
hence f . x misses f . y by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence f is disjoint_valued by PROB_2:def_2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines disjoint_valued DYNKIN:def_2_:_
for Omega being non empty set
for f being SetSequence of Omega holds
( f is disjoint_valued iff for n, m being Element of NAT st n < m holds
f . n misses f . m );
theorem Th4: :: DYNKIN:4
for Y being non empty set
for x being set holds
( x c= meet Y iff for y being Element of Y holds x c= y )
proof
let Y be non empty set ; ::_thesis: for x being set holds
( x c= meet Y iff for y being Element of Y holds x c= y )
let x be set ; ::_thesis: ( x c= meet Y iff for y being Element of Y holds x c= y )
hereby ::_thesis: ( ( for y being Element of Y holds x c= y ) implies x c= meet Y )
assume A1: x c= meet Y ; ::_thesis: for y being Element of Y holds x c= y
let y be Element of Y; ::_thesis: x c= y
for z being set st z in x holds
z in y by A1, SETFAM_1:def_1;
hence x c= y by TARSKI:def_3; ::_thesis: verum
end;
assume A2: for y being Element of Y holds x c= y ; ::_thesis: x c= meet Y
for z being set st z in x holds
z in meet Y
proof
let z be set ; ::_thesis: ( z in x implies z in meet Y )
assume A3: z in x ; ::_thesis: z in meet Y
now__::_thesis:_for_u_being_set_st_u_in_Y_holds_
z_in_u
let u be set ; ::_thesis: ( u in Y implies z in u )
assume u in Y ; ::_thesis: z in u
then x c= u by A2;
hence z in u by A3; ::_thesis: verum
end;
hence z in meet Y by SETFAM_1:def_1; ::_thesis: verum
end;
hence x c= meet Y by TARSKI:def_3; ::_thesis: verum
end;
notation
let x be set ;
synonym intersection_stable x for 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 :: DYNKIN:def 3
(f . n) \ (union (rng (f | n)));
coherence
(f . n) \ (union (rng (f | n))) is Subset of Omega ;
end;
:: deftheorem defines disjointify DYNKIN:def_3_:_
for Omega being non empty set
for f being SetSequence of Omega
for n being Nat holds disjointify (f,n) = (f . n) \ (union (rng (f | n)));
definition
let Omega be non empty set ;
let g be SetSequence of Omega;
func disjointify g -> SetSequence of Omega means :Def4: :: DYNKIN:def 4
for n being Nat holds it . n = disjointify (g,n);
existence
ex b1 being SetSequence of Omega st
for n being Nat holds b1 . n = disjointify (g,n)
proof
deffunc H1( Nat) -> Subset of Omega = disjointify (g,$1);
consider f being Function of NAT,(bool Omega) such that
A1: for x being Element of NAT holds f . x = H1(x) from FUNCT_2:sch_4();
take f ; ::_thesis: for n being Nat holds f . n = disjointify (g,n)
let n be Nat; ::_thesis: f . n = disjointify (g,n)
n in NAT by ORDINAL1:def_12;
hence f . n = disjointify (g,n) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being SetSequence of Omega st ( for n being Nat holds b1 . n = disjointify (g,n) ) & ( for n being Nat holds b2 . n = disjointify (g,n) ) holds
b1 = b2
proof
let i1, i2 be SetSequence of Omega; ::_thesis: ( ( for n being Nat holds i1 . n = disjointify (g,n) ) & ( for n being Nat holds i2 . n = disjointify (g,n) ) implies i1 = i2 )
assume A2: for n being Nat holds i1 . n = disjointify (g,n) ; ::_thesis: ( ex n being Nat st not i2 . n = disjointify (g,n) or i1 = i2 )
assume A3: for n being Nat holds i2 . n = disjointify (g,n) ; ::_thesis: i1 = i2
now__::_thesis:_for_n_being_Element_of_NAT_holds_i1_._n_=_i2_._n
let n be Element of NAT ; ::_thesis: i1 . n = i2 . n
i1 . n = disjointify (g,n) by A2;
hence i1 . n = i2 . n by A3; ::_thesis: verum
end;
hence i1 = i2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines disjointify DYNKIN:def_4_:_
for Omega being non empty set
for g, b3 being SetSequence of Omega holds
( b3 = disjointify g iff for n being Nat holds b3 . n = disjointify (g,n) );
theorem Th5: :: DYNKIN:5
for Omega being non empty set
for f being SetSequence of Omega
for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n)))
proof
let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega
for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n)))
let f be SetSequence of Omega; ::_thesis: for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n)))
let n be Nat; ::_thesis: (disjointify f) . n = (f . n) \ (union (rng (f | n)))
(disjointify f) . n = disjointify (f,n) by Def4;
hence (disjointify f) . n = (f . n) \ (union (rng (f | n))) ; ::_thesis: verum
end;
theorem Th6: :: DYNKIN:6
for Omega being non empty set
for f being SetSequence of Omega holds disjointify f is V56()
proof
let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega holds disjointify f is V56()
let f be SetSequence of Omega; ::_thesis: disjointify f is V56()
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<_m_holds_
(disjointify_f)_._n_misses_(disjointify_f)_._m
let n, m be Element of NAT ; ::_thesis: ( n < m implies (disjointify f) . n misses (disjointify f) . m )
assume n < m ; ::_thesis: (disjointify f) . n misses (disjointify f) . m
then A1: n in 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 Th5;
(f . n) \ (union (rng (f | n))) c= f . n by XBOOLE_1:36;
then (disjointify f) . n c= f . n by Th5;
hence (disjointify f) . n misses (disjointify f) . m by A3, XBOOLE_1:63; ::_thesis: verum
end;
hence disjointify f is V56() by Def2; ::_thesis: verum
end;
theorem Th7: :: DYNKIN:7
for Omega being non empty set
for f being SetSequence of Omega holds union (rng (disjointify f)) = union (rng f)
proof
let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega holds union (rng (disjointify f)) = union (rng f)
let f be SetSequence of Omega; ::_thesis: union (rng (disjointify f)) = union (rng f)
A1: dom f = NAT by FUNCT_2:def_1;
A2: dom (disjointify f) = NAT by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_union_(rng_f)_holds_
x_in_union_(rng_(disjointify_f))
let x be set ; ::_thesis: ( x in union (rng f) implies x in union (rng (disjointify f)) )
defpred S1[ Nat] means x in f . $1;
assume x in union (rng f) ; ::_thesis: x in union (rng (disjointify f))
then consider y being set such that
A3: x in y and
A4: y in rng f by TARSKI:def_4;
consider z being set 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 S1[k]
proof
take n ; ::_thesis: S1[n]
thus S1[n] by A3, A6; ::_thesis: verum
end;
consider k being Nat such that
A8: ( S1[k] & ( for m being Nat st S1[m] holds
k <= m ) ) from NAT_1:sch_5(A7);
now__::_thesis:_not_x_in_union_(rng_(f_|_k))
assume x in union (rng (f | k)) ; ::_thesis: contradiction
then consider y being set such that
A9: x in y and
A10: y in rng (f | k) by TARSKI:def_4;
consider z being set 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= 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; ::_thesis: verum
end;
then x in (f . k) \ (union (rng (f | k))) by A8, XBOOLE_0:def_5;
then A13: x in (disjointify f) . k by Th5;
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; ::_thesis: verum
end;
then A14: union (rng f) c= union (rng (disjointify f)) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_union_(rng_(disjointify_f))_holds_
x_in_union_(rng_f)
let x be set ; ::_thesis: ( x in union (rng (disjointify f)) implies x in union (rng f) )
assume x in union (rng (disjointify f)) ; ::_thesis: x in union (rng f)
then consider y being set such that
A15: x in y and
A16: y in rng (disjointify f) by TARSKI:def_4;
consider z being set 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, Th5;
hence x in union (rng f) by A19, TARSKI:def_4; ::_thesis: verum
end;
then union (rng (disjointify f)) c= union (rng f) by TARSKI:def_3;
hence union (rng (disjointify f)) = union (rng f) by A14, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th8: :: DYNKIN:8
for Omega being non empty set
for x, y being Subset of Omega st x misses y holds
(x,y) followed_by ({} Omega) is V56()
proof
let Omega be non empty set ; ::_thesis: for x, y being Subset of Omega st x misses y holds
(x,y) followed_by ({} Omega) is V56()
let x, y be Subset of Omega; ::_thesis: ( x misses y implies (x,y) followed_by ({} Omega) is V56() )
assume A1: x misses y ; ::_thesis: (x,y) followed_by ({} Omega) is V56()
reconsider r = (x,y) followed_by ({} Omega) as Function of NAT,(bool Omega) ;
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<_m_holds_
r_._n_misses_r_._m
let n, m be Element of NAT ; ::_thesis: ( n < m implies r . n misses r . m )
A2: ( m > 1 implies r . m = {} ) by FUNCT_7:124;
assume A3: n < m ; ::_thesis: r . n misses r . m
A4: now__::_thesis:_(_(_m_=_0_or_m_=_1_)_implies_(_n_=_0_&_m_=_1_)_)
assume A5: ( m = 0 or m = 1 ) ; ::_thesis: ( n = 0 & 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; ::_thesis: verum
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; ::_thesis: verum
end;
hence (x,y) followed_by ({} Omega) is V56() by Def2; ::_thesis: verum
end;
theorem Th9: :: DYNKIN:9
for Omega being non empty set
for f being SetSequence of Omega st f is V56() holds
for X being Subset of Omega holds seqIntersection (X,f) is V56()
proof
let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega st f is V56() holds
for X being Subset of Omega holds seqIntersection (X,f) is V56()
let f be SetSequence of Omega; ::_thesis: ( f is V56() implies for X being Subset of Omega holds seqIntersection (X,f) is V56() )
assume A1: f is V56() ; ::_thesis: for X being Subset of Omega holds seqIntersection (X,f) is V56()
let X be Subset of Omega; ::_thesis: seqIntersection (X,f) is V56()
for n, m being Element of NAT st n < m holds
(seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m
proof
let n, m be Element of NAT ; ::_thesis: ( n < m implies (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m )
assume n < m ; ::_thesis: (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m
then f . n misses f . m by A1, PROB_2:def_2;
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 (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m by A2, XBOOLE_1:74; ::_thesis: verum
end;
hence seqIntersection (X,f) is V56() by Def2; ::_thesis: verum
end;
theorem Th10: :: DYNKIN:10
for Omega being non empty set
for f being SetSequence of Omega
for X being Subset of Omega holds X /\ (Union f) = Union (seqIntersection (X,f))
proof
let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega
for X being Subset of Omega holds X /\ (Union f) = Union (seqIntersection (X,f))
let f be SetSequence of Omega; ::_thesis: for X being Subset of Omega holds X /\ (Union f) = Union (seqIntersection (X,f))
let X be Subset of Omega; ::_thesis: X /\ (Union f) = Union (seqIntersection (X,f))
A1: dom f = NAT by FUNCT_2:def_1;
now__::_thesis:_for_z_being_set_st_z_in_Union_(seqIntersection_(X,f))_holds_
z_in_X_/\_(Union_f)
reconsider g = seqIntersection (X,f) as SetSequence of Omega ;
let z be set ; ::_thesis: ( z in Union (seqIntersection (X,f)) implies z in X /\ (Union f) )
assume z in Union (seqIntersection (X,f)) ; ::_thesis: z in X /\ (Union f)
then consider u being set such that
A2: z in u and
A3: u in rng g by TARSKI:def_4;
consider v being set 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; ::_thesis: verum
end;
then A9: Union (seqIntersection (X,f)) c= X /\ (Union f) by TARSKI:def_3;
A10: dom (seqIntersection (X,f)) = NAT by FUNCT_2:def_1;
now__::_thesis:_for_z_being_set_st_z_in_X_/\_(Union_f)_holds_
z_in_Union_(seqIntersection_(X,f))
let z be set ; ::_thesis: ( z in X /\ (Union f) implies z in Union (seqIntersection (X,f)) )
assume A11: z in X /\ (Union f) ; ::_thesis: z in Union (seqIntersection (X,f))
then z in union (rng f) by XBOOLE_0:def_4;
then consider u being set such that
A12: z in u and
A13: u in rng f by TARSKI:def_4;
consider v being set 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; ::_thesis: verum
end;
then X /\ (Union f) c= Union (seqIntersection (X,f)) by TARSKI:def_3;
hence X /\ (Union f) = Union (seqIntersection (X,f)) by A9, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
definition
let Omega be non empty set ;
mode Dynkin_System of Omega -> Subset-Family of Omega means :Def5: :: DYNKIN:def 5
( ( for f being SetSequence of Omega st rng f c= it & f is V56() holds
Union f in it ) & ( for X being Subset of Omega st X in it holds
X ` in it ) & {} in it );
existence
ex b1 being Subset-Family of Omega st
( ( for f being SetSequence of Omega st rng f c= b1 & f is V56() holds
Union f in b1 ) & ( for X being Subset of Omega st X in b1 holds
X ` in b1 ) & {} in b1 )
proof
reconsider D = bool Omega as non empty Subset-Family of Omega ;
take D ; ::_thesis: ( ( for f being SetSequence of Omega st rng f c= D & f is V56() holds
Union f in D ) & ( for X being Subset of Omega st X in D holds
X ` in D ) & {} in D )
{} c= Omega by XBOOLE_1:2;
hence ( ( for f being SetSequence of Omega st rng f c= D & f is V56() holds
Union f in D ) & ( for X being Subset of Omega st X in D holds
X ` in D ) & {} in D ) ; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines Dynkin_System DYNKIN:def_5_:_
for Omega being non empty set
for b2 being Subset-Family of Omega holds
( b2 is Dynkin_System of Omega iff ( ( for f being SetSequence of Omega st rng f c= b2 & f is V56() holds
Union f in b2 ) & ( for X being Subset of Omega st X in b2 holds
X ` in b2 ) & {} in b2 ) );
registration
let Omega be non empty set ;
cluster -> non empty for Dynkin_System of Omega;
coherence
for b1 being Dynkin_System of Omega holds not b1 is empty by Def5;
end;
theorem Th11: :: DYNKIN:11
for Omega being non empty set holds bool Omega is Dynkin_System of Omega
proof
let Omega be non empty set ; ::_thesis: bool Omega is Dynkin_System of Omega
A1: ( {} c= Omega & bool Omega c= bool Omega ) by XBOOLE_1:2;
( ( for f being SetSequence of Omega st rng f c= bool Omega & f is V56() holds
Union f in bool Omega ) & ( for X being Subset of Omega st X in bool Omega holds
X ` in bool Omega ) ) ;
hence bool Omega is Dynkin_System of Omega by A1, Def5; ::_thesis: verum
end;
theorem Th12: :: DYNKIN:12
for F, Omega being non empty set st ( for Y being set st Y in F holds
Y is Dynkin_System of Omega ) holds
meet F is Dynkin_System of Omega
proof
let F, Omega be non empty set ; ::_thesis: ( ( for Y being set st Y in F holds
Y is Dynkin_System of Omega ) implies meet F is Dynkin_System of Omega )
assume A1: for Y being set st Y in F holds
Y is Dynkin_System of Omega ; ::_thesis: meet F is Dynkin_System of Omega
now__::_thesis:_for_Y_being_set_st_Y_in_F_holds_
{}_in_Y
let Y be set ; ::_thesis: ( Y in F implies {} in Y )
assume Y in F ; ::_thesis: {} in Y
then Y is Dynkin_System of Omega by A1;
hence {} in Y by Def5; ::_thesis: verum
end;
then A2: {} in meet F by SETFAM_1:def_1;
A3: now__::_thesis:_for_f_being_SetSequence_of_Omega_st_rng_f_c=_meet_F_&_f_is_V56()_holds_
Union_f_in_meet_F
let f be SetSequence of Omega; ::_thesis: ( rng f c= meet F & f is V56() implies Union f in meet F )
assume that
A4: rng f c= meet F and
A5: f is V56() ; ::_thesis: Union f in meet F
now__::_thesis:_for_Y_being_set_st_Y_in_F_holds_
Union_f_in_Y
let Y be set ; ::_thesis: ( Y in F implies Union f in Y )
assume A6: Y in F ; ::_thesis: Union f in Y
meet F c= Y by A6, SETFAM_1:3;
then A7: rng f c= Y by A4, XBOOLE_1:1;
Y is Dynkin_System of Omega by A1, A6;
hence Union f in Y by A5, A7, Def5; ::_thesis: verum
end;
hence Union f in meet F by SETFAM_1:def_1; ::_thesis: verum
end;
A8: now__::_thesis:_for_X_being_Subset_of_Omega_st_X_in_meet_F_holds_
X_`_in_meet_F
let X be Subset of Omega; ::_thesis: ( X in meet F implies X ` in meet F )
assume A9: X in meet F ; ::_thesis: X ` in meet F
for Y being set st Y in F holds
X ` in Y
proof
let Y be set ; ::_thesis: ( Y in F implies X ` in Y )
assume Y in F ; ::_thesis: X ` in Y
then ( Y is Dynkin_System of Omega & meet F c= Y ) by A1, SETFAM_1:3;
hence X ` in Y by A9, Def5; ::_thesis: verum
end;
hence X ` in meet F by SETFAM_1:def_1; ::_thesis: verum
end;
set Y = the Element of F;
A10: meet F c= the Element of F by SETFAM_1:3;
the Element of F is Dynkin_System of Omega by A1;
then meet F is Subset-Family of Omega by A10, XBOOLE_1:1;
hence meet F is Dynkin_System of Omega by A3, A8, A2, Def5; ::_thesis: verum
end;
theorem Th13: :: DYNKIN:13
for Omega being non empty set
for A, B being Subset of Omega
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \ B in D
proof
let Omega be non empty set ; ::_thesis: for A, B being Subset of Omega
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \ B in D
let A, B be Subset of Omega; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \ B in D
let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D implies A \ B in D )
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; ::_thesis: ( not A in D or not B in D or A \ B in D )
assume that
A3: A in D and
A4: B in D ; ::_thesis: A \ B in D
B ` in D by A1, A4, Def5;
then A /\ (B `) in D by A2, A3, FINSUB_1:def_2;
hence A \ B in D by SUBSET_1:13; ::_thesis: verum
end;
theorem Th14: :: DYNKIN:14
for Omega being non empty set
for A, B being Subset of Omega
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \/ B in D
proof
let Omega be non empty set ; ::_thesis: for A, B being Subset of Omega
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \/ B in D
let A, B be Subset of Omega; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \/ B in D
let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D implies A \/ B in D )
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; ::_thesis: ( not A in D or not B in D or A \/ B in D )
assume ( A in D & B in D ) ; ::_thesis: A \/ 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 A \/ B in D ; ::_thesis: verum
end;
theorem Th15: :: DYNKIN:15
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for x being finite set st x c= D holds
union x in D
proof
let Omega be non empty set ; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for x being finite set st x c= D holds
union x in D
let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies for x being finite set st x c= D holds
union x in D )
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; ::_thesis: for x being finite set st x c= D holds
union x in D
defpred S1[ set ] means union $1 in D;
let x be finite set ; ::_thesis: ( x c= D implies union x in D )
assume A3: x c= D ; ::_thesis: union x in D
A4: for y, b being set st y in x & b c= x & S1[b] holds
S1[b \/ {y}]
proof
let y, b be set ; ::_thesis: ( y in x & b c= x & S1[b] implies S1[b \/ {y}] )
assume that
A5: y in x and
b c= x and
A6: union b in D ; ::_thesis: S1[b \/ {y}]
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, Th14, ZFMISC_1:25;
hence S1[b \/ {y}] by ZFMISC_1:78; ::_thesis: verum
end;
A7: x is finite ;
A8: S1[ {} ] by A1, Def5, ZFMISC_1:2;
thus S1[x] from FINSET_1:sch_2(A7, A8, A4); ::_thesis: verum
end;
theorem Th16: :: DYNKIN:16
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D
proof
let Omega be non empty set ; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D
let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D )
assume A1: ( D is Dynkin_System of Omega & D is intersection_stable ) ; ::_thesis: for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D
let f be SetSequence of Omega; ::_thesis: ( rng f c= D implies rng (disjointify f) c= D )
assume A2: rng f c= D ; ::_thesis: rng (disjointify f) c= D
A3: for n being Element of NAT holds (disjointify f) . n in D
proof
let n be Element of NAT ; ::_thesis: (disjointify f) . n in D
A4: rng (f | n) c= rng f by RELAT_1:70;
( dom (f | n) c= Segm n & rng f is Subset-Family of Omega ) by RELAT_1:58, RELAT_1:def_19;
then rng (f | n) is finite Subset-Family of Omega by A4, XBOOLE_1:1;
then A5: union (rng (f | n)) in D by A1, A2, A4, Th15, 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, Th13;
hence (disjointify f) . n in D by Th5; ::_thesis: verum
end;
now__::_thesis:_for_y_being_set_st_y_in_rng_(disjointify_f)_holds_
y_in_D
let y be set ; ::_thesis: ( y in rng (disjointify f) implies y in D )
assume y in rng (disjointify f) ; ::_thesis: y in D
then consider x being set 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; ::_thesis: verum
end;
hence rng (disjointify f) c= D by TARSKI:def_3; ::_thesis: verum
end;
theorem Th17: :: DYNKIN:17
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D
proof
let Omega be non empty set ; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D
let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D )
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; ::_thesis: for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D
let f be SetSequence of Omega; ::_thesis: ( rng f c= D implies union (rng f) in D )
assume rng f c= D ; ::_thesis: union (rng f) in D
then A3: rng (disjointify f) c= D by A1, A2, Th16;
disjointify f is V56() by Th6;
then Union (disjointify f) in D by A1, A3, Def5;
hence union (rng f) in D by Th7; ::_thesis: verum
end;
theorem Th18: :: DYNKIN:18
for Omega being non empty set
for D being Dynkin_System of Omega
for x, y being Element of D st x misses y holds
x \/ y in D
proof
let Omega be non empty set ; ::_thesis: for D being Dynkin_System of Omega
for x, y being Element of D st x misses y holds
x \/ y in D
let D be Dynkin_System of Omega; ::_thesis: for x, y being Element of D st x misses y holds
x \/ y in D
reconsider e = {} as Element of D by Def5;
let x, y be Element of D; ::_thesis: ( x misses y implies x \/ y in 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 Function of NAT,D by Lm1;
then A1: rng r c= D by RELAT_1:def_19;
assume x misses y ; ::_thesis: x \/ y in D
then r is V56() by Th8;
then Union r in D by A1, Def5;
hence x \/ y in D by Th3; ::_thesis: verum
end;
theorem Th19: :: DYNKIN:19
for Omega being non empty set
for D being Dynkin_System of Omega
for x, y being Element of D st x c= y holds
y \ x in D
proof
let Omega be non empty set ; ::_thesis: for D being Dynkin_System of Omega
for x, y being Element of D st x c= y holds
y \ x in D
let D be Dynkin_System of Omega; ::_thesis: for x, y being Element of D st x c= y holds
y \ x in D
let x, y be Element of D; ::_thesis: ( x c= y implies y \ x in D )
A1: (x \/ (y `)) ` = (x `) /\ ((y `) `) by XBOOLE_1:53
.= y \ x by SUBSET_1:13 ;
assume x c= y ; ::_thesis: y \ x in D
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, Th18;
hence y \ x in D by A1, Def5; ::_thesis: verum
end;
begin
theorem Th20: :: DYNKIN:20
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
D is SigmaField of Omega
proof
let Omega be non empty set ; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
D is SigmaField of Omega
let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies D is SigmaField of Omega )
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; ::_thesis: D is SigmaField of Omega
A3: for f being SetSequence of Omega st rng f c= D holds
Intersection f in D
proof
let f be SetSequence of Omega; ::_thesis: ( rng f c= D implies Intersection f in D )
assume A4: rng f c= D ; ::_thesis: Intersection f in D
A5: for n being Element of NAT holds (f . n) ` in D
proof
let n be Element of NAT ; ::_thesis: (f . n) ` in D
f . n in rng f by NAT_1:51;
hence (f . n) ` in D by A1, A4, Def5; ::_thesis: verum
end;
A6: for n being Element of NAT holds (Complement f) . n in D
proof
let n be Element of NAT ; ::_thesis: (Complement f) . n in D
(Complement f) . n = (f . n) ` by PROB_1:def_2;
hence (Complement f) . n in D by A5; ::_thesis: verum
end;
for x being set st x in rng (Complement f) holds
x in D
proof
let x be set ; ::_thesis: ( x in rng (Complement f) implies x in D )
assume x in rng (Complement f) ; ::_thesis: x in D
then consider z being set 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 x in D by A6; ::_thesis: verum
end;
then rng (Complement f) c= D by TARSKI:def_3;
then Union (Complement f) in D by A1, A2, Th17;
then (Union (Complement f)) ` in D by A1, Def5;
hence Intersection f in D by PROB_1:def_3; ::_thesis: verum
end;
for X being Subset of Omega st X in D holds
X ` in D by A1, Def5;
hence D is SigmaField of Omega by A3, PROB_1:15; ::_thesis: verum
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: :: DYNKIN:def 6
( E c= it & ( for D being Dynkin_System of Omega st E c= D holds
it c= D ) );
existence
ex b1 being Dynkin_System of Omega st
( E c= b1 & ( for D being Dynkin_System of Omega st E c= D holds
b1 c= D ) )
proof
defpred S1[ set ] means ( $1 is Dynkin_System of Omega & E c= $1 );
consider Y being set such that
A1: for x being set holds
( x in Y iff ( x in bool (bool Omega) & S1[x] ) ) from XBOOLE_0:sch_1();
bool Omega is Dynkin_System of Omega by Th11;
then reconsider Y = Y as non empty set by A1;
for z being set st z in Y holds
z is Dynkin_System of Omega by A1;
then reconsider I = meet Y as Dynkin_System of Omega by Th12;
take I ; ::_thesis: ( E c= I & ( for D being Dynkin_System of Omega st E c= D holds
I c= D ) )
for y being Element of Y holds E c= y by A1;
hence E c= I by Th4; ::_thesis: for D being Dynkin_System of Omega st E c= D holds
I c= D
let D be Dynkin_System of Omega; ::_thesis: ( E c= D implies I c= D )
assume E c= D ; ::_thesis: I c= D
then D in Y by A1;
hence I c= D by SETFAM_1:3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Dynkin_System of Omega st E c= b1 & ( for D being Dynkin_System of Omega st E c= D holds
b1 c= D ) & E c= b2 & ( for D being Dynkin_System of Omega st E c= D holds
b2 c= D ) holds
b1 = b2
proof
let I1, I2 be Dynkin_System of Omega; ::_thesis: ( E c= I1 & ( for D being Dynkin_System of Omega st E c= D holds
I1 c= D ) & E c= I2 & ( for D being Dynkin_System of Omega st E c= D holds
I2 c= D ) implies I1 = I2 )
assume A2: ( E c= I1 & ( for D being Dynkin_System of Omega st E c= D holds
I1 c= D ) ) ; ::_thesis: ( not E c= I2 or ex D being Dynkin_System of Omega st
( E c= D & not I2 c= D ) or I1 = I2 )
assume ( E c= I2 & ( for D being Dynkin_System of Omega st E c= D holds
I2 c= D ) ) ; ::_thesis: I1 = I2
then ( I1 c= I2 & I2 c= I1 ) by A2;
hence I1 = I2 by XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines generated_Dynkin_System DYNKIN:def_6_:_
for Omega being non empty set
for E being Subset-Family of Omega
for b3 being Dynkin_System of Omega holds
( b3 = generated_Dynkin_System E iff ( E c= b3 & ( for D being Dynkin_System of Omega st E c= D holds
b3 c= D ) ) );
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: :: DYNKIN:def 7
for A being Subset of Omega holds
( A in it iff A /\ X in G );
existence
ex b1 being Subset-Family of Omega st
for A being Subset of Omega holds
( A in b1 iff A /\ X in G )
proof
defpred S1[ set ] means $1 /\ X in G;
consider I being set such that
A1: for x being set holds
( x in I iff ( x in bool Omega & S1[x] ) ) from XBOOLE_0:sch_1();
for x being set st x in I holds
x in bool Omega by A1;
then reconsider I = I as Subset-Family of Omega by TARSKI:def_3;
take I ; ::_thesis: for A being Subset of Omega holds
( A in I iff A /\ X in G )
let A be Subset of Omega; ::_thesis: ( A in I iff A /\ X in G )
thus ( A in I iff A /\ X in G ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of Omega st ( for A being Subset of Omega holds
( A in b1 iff A /\ X in G ) ) & ( for A being Subset of Omega holds
( A in b2 iff A /\ X in G ) ) holds
b1 = b2
proof
let I1, I2 be Subset-Family of Omega; ::_thesis: ( ( for A being Subset of Omega holds
( A in I1 iff A /\ X in G ) ) & ( for A being Subset of Omega holds
( A in I2 iff A /\ X in G ) ) implies I1 = I2 )
assume A2: for A being Subset of Omega holds
( A in I1 iff A /\ X in G ) ; ::_thesis: ( ex A being Subset of Omega st
( ( A in I2 implies A /\ X in G ) implies ( A /\ X in G & not A in I2 ) ) or I1 = I2 )
assume A3: for A being Subset of Omega holds
( A in I2 iff A /\ X in G ) ; ::_thesis: I1 = I2
now__::_thesis:_for_A_being_Subset_of_Omega_holds_
(_A_in_I1_iff_A_in_I2_)
let A be Subset of Omega; ::_thesis: ( A in I1 iff A in I2 )
( A in I1 iff A /\ X in G ) by A2;
hence ( A in I1 iff A in I2 ) by A3; ::_thesis: verum
end;
hence I1 = I2 by SUBSET_1:3; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines DynSys DYNKIN:def_7_:_
for Omega being non empty set
for G being set
for X being Subset of Omega
for b4 being Subset-Family of Omega holds
( b4 = DynSys (X,G) iff for A being Subset of Omega holds
( A in b4 iff A /\ X in G ) );
definition
let Omega be non empty set ;
let G be Dynkin_System of Omega;
let X be Element of G;
:: original: DynSys
redefine func DynSys (X,G) -> Dynkin_System of Omega;
coherence
DynSys (X,G) is Dynkin_System of Omega
proof
A1: for f being SetSequence of Omega st rng f c= DynSys (X,G) & f is V56() holds
Union f in DynSys (X,G)
proof
reconsider X1 = X as Subset of Omega ;
let f be SetSequence of Omega; ::_thesis: ( rng f c= DynSys (X,G) & f is V56() implies Union f in DynSys (X,G) )
assume that
A2: rng f c= DynSys (X,G) and
A3: f is V56() ; ::_thesis: Union f in DynSys (X,G)
now__::_thesis:_for_x_being_set_st_x_in_rng_(seqIntersection_(X1,f))_holds_
x_in_G
let x be set ; ::_thesis: ( x in rng (seqIntersection (X1,f)) implies x in G )
assume x in rng (seqIntersection (X1,f)) ; ::_thesis: x in G
then consider n being Element of NAT 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; ::_thesis: verum
end;
then A6: rng (seqIntersection (X1,f)) c= G by TARSKI:def_3;
seqIntersection (X,f) is V56() by A3, Th9;
then Union (seqIntersection (X1,f)) in G by A6, Def5;
then X /\ (Union f) in G by Th10;
hence Union f in DynSys (X,G) by Def7; ::_thesis: verum
end;
A7: for A being Subset of Omega st A in DynSys (X,G) holds
A ` in DynSys (X,G)
proof
let A be Subset of Omega; ::_thesis: ( A in DynSys (X,G) implies A ` in DynSys (X,G) )
X misses X ` by XBOOLE_1:79;
then A8: X /\ (X `) = {} by XBOOLE_0:def_7;
assume A in DynSys (X,G) ; ::_thesis: A ` in DynSys (X,G)
then X /\ A in G by Def7;
then A9: X \ (X /\ A) in G by Th19, 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 A ` in DynSys (X,G) by A9, Def7; ::_thesis: verum
end;
( {} /\ X = {} & {} in G ) by Def5;
then {} in DynSys (X,G) by Def7;
hence DynSys (X,G) is Dynkin_System of Omega by A1, A7, Def5; ::_thesis: verum
end;
end;
theorem Th21: :: DYNKIN:21
for Omega being non empty set
for E being Subset-Family of Omega
for X, Y being Subset of Omega st X in E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
proof
let Omega be non empty set ; ::_thesis: for E being Subset-Family of Omega
for X, Y being Subset of Omega st X in E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
let E be Subset-Family of Omega; ::_thesis: for X, Y being Subset of Omega st X in E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
let X, Y be Subset of Omega; ::_thesis: ( X in E & Y in generated_Dynkin_System E & E is intersection_stable implies X /\ Y in generated_Dynkin_System E )
assume that
A1: X in E and
A2: Y in generated_Dynkin_System E and
A3: E is intersection_stable ; ::_thesis: X /\ Y in generated_Dynkin_System E
reconsider G = generated_Dynkin_System E as Dynkin_System of Omega ;
E c= generated_Dynkin_System E by Def6;
then reconsider X = X as Element of G by A1;
for x being set st x in E holds
x in DynSys (X,G)
proof
let x be set ; ::_thesis: ( x in E implies x in DynSys (X,G) )
assume A4: x in E ; ::_thesis: x in DynSys (X,G)
then reconsider x = x as Subset of Omega ;
A5: E c= G by Def6;
x /\ X in E by A1, A3, A4, FINSUB_1:def_2;
hence x in DynSys (X,G) by A5, Def7; ::_thesis: verum
end;
then E c= DynSys (X,G) by TARSKI:def_3;
then generated_Dynkin_System E c= DynSys (X,G) by Def6;
hence X /\ Y in generated_Dynkin_System E by A2, Def7; ::_thesis: verum
end;
theorem Th22: :: DYNKIN:22
for Omega being non empty set
for E being Subset-Family of Omega
for X, Y being Subset of Omega st X in generated_Dynkin_System E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
proof
let Omega be non empty set ; ::_thesis: for E being Subset-Family of Omega
for X, Y being Subset of Omega st X in generated_Dynkin_System E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
let E be Subset-Family of Omega; ::_thesis: for X, Y being Subset of Omega st X in generated_Dynkin_System E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
let X, Y be Subset of Omega; ::_thesis: ( X in generated_Dynkin_System E & Y in generated_Dynkin_System E & E is intersection_stable implies X /\ Y in generated_Dynkin_System E )
assume that
A1: X in generated_Dynkin_System E and
A2: Y in generated_Dynkin_System E and
A3: E is intersection_stable ; ::_thesis: X /\ Y in generated_Dynkin_System E
reconsider G = generated_Dynkin_System E as Dynkin_System of Omega ;
defpred S1[ set ] means ex X being Element of G st $1 = DynSys (X,G);
consider h being set such that
A4: for x being set holds
( x in h iff ( x in bool (bool Omega) & S1[x] ) ) from XBOOLE_0:sch_1();
A5: for Y being set st Y in h holds
Y is Dynkin_System of Omega
proof
let Y be set ; ::_thesis: ( Y in h implies Y is Dynkin_System of Omega )
assume Y in h ; ::_thesis: Y is Dynkin_System of Omega
then ex X being Element of G st Y = DynSys (X,G) by A4;
hence Y is Dynkin_System of Omega ; ::_thesis: verum
end;
not h is empty
proof
set X = the Element of G;
DynSys ( the Element of G,G) in h by A4;
hence not h is empty ; ::_thesis: verum
end;
then reconsider h = 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 set st x in E holds
x in meet h
proof
let x be set ; ::_thesis: ( x in E implies x in meet h )
assume A7: x in E ; ::_thesis: x in meet h
for Y being set st Y in h holds
x in Y
proof
let Y be set ; ::_thesis: ( Y in h implies x in Y )
assume Y in h ; ::_thesis: x in Y
then consider X being Element of G such that
A8: Y = DynSys (X,G) by A4;
x /\ X in G by A3, A7, Th21;
hence x in Y by A7, A8, Def7; ::_thesis: verum
end;
hence x in meet h by SETFAM_1:def_1; ::_thesis: verum
end;
then A9: E c= meet h by TARSKI:def_3;
meet h is Dynkin_System of Omega by A5, Th12;
then G c= meet h by A9, Def6;
then G c= DynSys (X,G) by A6, XBOOLE_1:1;
hence X /\ Y in generated_Dynkin_System E by A2, Def7; ::_thesis: verum
end;
theorem Th23: :: DYNKIN:23
for Omega being non empty set
for E being Subset-Family of Omega st E is intersection_stable holds
generated_Dynkin_System E is intersection_stable
proof
let Omega be non empty set ; ::_thesis: for E being Subset-Family of Omega st E is intersection_stable holds
generated_Dynkin_System E is intersection_stable
let E be Subset-Family of Omega; ::_thesis: ( E is intersection_stable implies generated_Dynkin_System E is intersection_stable )
assume A1: E is intersection_stable ; ::_thesis: generated_Dynkin_System 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, Th22;
hence generated_Dynkin_System E is intersection_stable by FINSUB_1:def_2; ::_thesis: verum
end;
theorem :: DYNKIN:24
for Omega being non empty set
for E being Subset-Family of Omega st E is intersection_stable holds
for D being Dynkin_System of Omega st E c= D holds
sigma E c= D
proof
let Omega be non empty set ; ::_thesis: for E being Subset-Family of Omega st E is intersection_stable holds
for D being Dynkin_System of Omega st E c= D holds
sigma E c= D
let E be Subset-Family of Omega; ::_thesis: ( E is intersection_stable implies for D being Dynkin_System of Omega st E c= D holds
sigma E c= D )
assume A1: E is intersection_stable ; ::_thesis: for D being Dynkin_System of Omega st E c= D holds
sigma E c= D
reconsider G = generated_Dynkin_System E as Dynkin_System of Omega ;
G is intersection_stable by A1, Th23;
then A2: G is SigmaField of Omega by Th20;
let D be Dynkin_System of Omega; ::_thesis: ( E c= D implies sigma E c= D )
assume E c= D ; ::_thesis: sigma 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 sigma E c= D by A3, XBOOLE_1:1; ::_thesis: verum
end;