The abstract of the Mizar article:

Dynkin's Lemma in Measure Theory

by

Franz Merkl

Received November 27, 2000

MML identifier: DYNKIN

[ Mizar article, MML identifier index ]

environ

 vocabulary PROB_1, RELAT_1, FUNCT_1, ALGSEQ_1, FINSET_1, BOOLE, FUNCOP_1,
      FUNCT_4, TARSKI, PROB_2, SETFAM_1, COHSP_1, SUBSET_1, DYNKIN;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, NUMBERS, XREAL_0,
      SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, NAT_1, FUNCT_4, FUNCOP_1, ALGSEQ_1,
      PROB_1, COHSP_1, PROB_2;
 constructors ALGSEQ_1, NAT_1, FUNCT_4, COHSP_1, PROB_2, MEMBERED;
 clusters SUBSET_1, ARYTM_3, RELSET_1, FINSET_1, FUNCT_1, FUNCT_4, FUNCOP_1,
      MEMBERED, NUMBERS, ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


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 of bool Omega,
        k,n,m for Nat,
        h,x,y,z,u,v,Y,I for set;

:::::::::::::::::::
:: Preliminaries ::
:::::::::::::::::::

theorem :: DYNKIN:1
 for f being SetSequence of Omega
  for x holds x in rng f iff ex n st f.n=x;

theorem :: DYNKIN:2
 for n holds PSeg(n) is finite;

definition let n;
 cluster PSeg(n) -> finite;
end;

definition
 let a,b,c be set;
 func (a,b) followed_by c equals
:: DYNKIN:def 1
 (NAT --> c) +* ((0,1) --> (a,b));
end;

definition
 let a,b,c be set;
 cluster (a,b) followed_by c -> Function-like Relation-like;
end;

definition
 let X be non empty set;
 let a,b,c be Element of X;
 redefine func (a,b) followed_by c -> Function of NAT, X;
end;

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

canceled 2;

theorem :: DYNKIN:5
for a,b,c being set holds
 ((a,b) followed_by c).0 = a &
 ((a,b) followed_by c).1 = b &
 for n st n <> 0 & n <> 1 holds
 ((a,b) followed_by c).n = c;

theorem :: DYNKIN:6
 for a,b being Subset of Omega holds
 union rng ((a,b) followed_by {}) = a \/ b;

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
:: DYNKIN:def 2
 for n holds it.n = X /\ f.n;
end;

begin
::::::::::::::::::::::::::::::::::::::::::::::::
:: disjoint-valued functions and intersection ::
::::::::::::::::::::::::::::::::::::::::::::::::

definition let Omega; let f;
  redefine attr f is disjoint_valued means
:: DYNKIN:def 3
    n<m implies f.n misses f.m;
end;

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

definition let x be set;
 redefine attr x is multiplicative;
 synonym x is intersection_stable;
end;

definition
  let Omega be non empty set;
  let f be SetSequence of Omega;
  let n be Element of NAT;
 canceled;

  func disjointify(f,n) -> Element of bool Omega equals
:: DYNKIN:def 5

  f.n \ union rng (f|PSeg(n));
end;

definition
 let Omega be non empty set;
 let g be SetSequence of Omega;
 func disjointify(g) -> SetSequence of Omega means
:: DYNKIN:def 6

 for n holds it.n=disjointify(g,n);
end;

theorem :: DYNKIN:8
 for n holds (disjointify(f)).n=f.n \ union rng(f|PSeg(n));

theorem :: DYNKIN:9
 for f being SetSequence of Omega holds
  disjointify(f) is disjoint_valued;

theorem :: DYNKIN:10
 for f being SetSequence of Omega holds
  union rng disjointify(f) = union rng f;

theorem :: DYNKIN:11
 for x,y being Subset of Omega st x misses y holds
  (x,y) followed_by {} Omega is disjoint_valued;

theorem :: DYNKIN:12
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;

theorem :: DYNKIN:13
for f being SetSequence of Omega
 for X being Subset of Omega holds
  X/\ Union f= Union seqIntersection(X,f);

begin

:::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Dynkin Systems:definition and closure properties ::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition let Omega;
  mode Dynkin_System of Omega -> Subset of bool Omega means
:: DYNKIN:def 7

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

definition let Omega;
  cluster -> non empty Dynkin_System of Omega;
end;

theorem :: DYNKIN:14
bool Omega is Dynkin_System of Omega;

theorem :: DYNKIN:15
  (for Y st Y in F holds Y is Dynkin_System of Omega) implies
  meet F is Dynkin_System of Omega;

theorem :: DYNKIN:16
 D is Dynkin_System of Omega & D is intersection_stable
 implies
 (A in D & B in D implies A\B in D);

theorem :: DYNKIN:17
 D is Dynkin_System of Omega & D is intersection_stable
 implies
 (A in D & B in D implies A \/ B in D);

theorem :: DYNKIN:18
 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;

theorem :: DYNKIN:19
  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;

theorem :: DYNKIN:20
 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;

theorem :: DYNKIN:21
 for D being Dynkin_System of Omega
  for x,y being Element of D holds
  x misses y implies x \/ y in D;

theorem :: DYNKIN:22
 for D being Dynkin_System of Omega
  for x,y being Element of D holds
  x c= y implies y\x in D;

begin

:::::::::::::::::::::::::::::::::::
:: Main steps for Dynkin's Lemma ::
:::::::::::::::::::::::::::::::::::

theorem :: DYNKIN:23
 D is Dynkin_System of Omega & D is intersection_stable implies
 D is SigmaField of Omega;

definition
 let Omega be non empty set;
 let E be Subset of bool Omega;
 func generated_Dynkin_System(E) -> Dynkin_System of Omega means
:: DYNKIN:def 8

 E c= it & for D being Dynkin_System of Omega holds
  (E c= D implies it c= D);
end;

definition
 let Omega be non empty set;
 let G be set;
 let X be Subset of Omega;
 func DynSys(X,G) -> Subset of bool Omega
 means
:: DYNKIN:def 9
 for A being Subset of Omega holds
  A in it iff A /\ X in G;
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;
end;

theorem :: DYNKIN:24
 for E being Subset of bool 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);

theorem :: DYNKIN:25
 for E being Subset of bool 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);

theorem :: DYNKIN:26
 for E being Subset of bool Omega st E is intersection_stable holds
  generated_Dynkin_System(E) is intersection_stable;

theorem :: DYNKIN:27
   for E being Subset of bool Omega st E is intersection_stable
  for D being Dynkin_System of Omega st E c= D holds
   sigma(E) c= D;