4.4. Measurable Space Generated by a Set of Sets🔗

Definition.

Let X be a set, and let \mathcal{F} \subseteq \mathcal{P}(X). We inductively define the sigma-algebra \gen (\mathcal{F}) on X, called the sigma-algebra generated by \mathcal{F}, as follows:

For any A \in \mathcal{F}, we have A \in \gen (\mathcal{F}).
\emptyset \in \gen (\mathcal{F}).
For any A \in \gen (\mathcal{F}), we have A^c \in \gen (\mathcal{F}).
For any sequence A_0, A_1, \dots \in \gen (\mathcal{F}), we have \bigcup_{n \in \mathbb{N}} A_n \in \gen (\mathcal{F}).

Lean code

/-- The smallest σ-algebra containing a collection `s` of basic sets -/
inductive GenerateMeasurable (s : Set (Set α)) : Set α → Prop
  | basic : ∀ u ∈ s, GenerateMeasurable s u
  | empty : GenerateMeasurable s ∅
  | compl : ∀ t, GenerateMeasurable s t → GenerateMeasurable s tᶜ
  | iUnion : ∀ f : ℕ → Set α, (∀ n, GenerateMeasurable s (f n)) →
      GenerateMeasurable s (⋃ i, f i)

/-- Construct the smallest measure space containing a collection of basic sets -/
def generateFrom (s : Set (Set α)) : MeasurableSpace α where
  MeasurableSet' := GenerateMeasurable s
  measurableSet_empty := .empty
  measurableSet_compl := .compl
  measurableSet_iUnion := .iUnion

Lemma (Induction Principle for Measurable Sets).

Let X be a measurable space, and let \mathcal{F} \subseteq \mathcal{P}(X). Suppose that \mathcal{M}(X) = \gen (\mathcal{F}). Let P(A) be a property on measurable sets A \subseteq X. Suppose that the following conditions hold:

For any A \in \mathcal{F}, we have P(A).
We have P(\emptyset).
For any measurable set A \subseteq X, we have P(A) implies P(A^c).
For any sequence of measurable sets A_0, A_1, \dots \subseteq X, we have \forall n \in \mathbb{N}, P(A_n) implies P\left(\bigcup_{n \in \mathbb{N}} A_n\right).

Then any measurable set A \subseteq X satisfies P(A).

Lean code

@[elab_as_elim]
theorem generateFrom_induction [MeasurableSpace α] (C : Set (Set α)) (h_eq : ‹_› = generateFrom C)
    (p : ∀ s : Set α, MeasurableSet s → Prop) (hC : ∀ t ∈ C, ∀ ht, p t ht)
    (empty : p (∅ : Set α) (MeasurableSet.empty)) (compl : ∀ t ht, p t ht → p tᶜ ht.compl)
    (iUnion : ∀ (s : ℕ → Set α) (hs : ∀ n, MeasurableSet (s n)),
      (∀ n, p (s n) (hs n)) → p (⋃ i, s i) (.iUnion hs)) (s : Set α)
    (hs : MeasurableSet s) : p s hs := byα:Type u_1inst✝:MeasurableSpace αC:Set (Set α)h_eq:inst✝ = generateFrom Cp:(s : Set α) → MeasurableSet s → ProphC:∀ t ∈ C, ∀ (ht : MeasurableSet t), p t htempty:p ∅ ⋯compl:∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯iUnion:∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ i, s i) ⋯s:Set αhs:MeasurableSet s⊢ p s hs
  rw [h_eq] at hsα:Type u_1inst✝:MeasurableSpace αC:Set (Set α)h_eq:inst✝ = generateFrom Cp:(s : Set α) → MeasurableSet s → ProphC:∀ t ∈ C, ∀ (ht : MeasurableSet t), p t htempty:p ∅ ⋯compl:∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯iUnion:∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ i, s i) ⋯s:Set αhs✝:MeasurableSet shs:MeasurableSet s⊢ p s hs
  induction hs with
  | basic t ht =>basicα:Type u_1inst✝:MeasurableSpace αC:Set (Set α)h_eq:inst✝ = generateFrom Cp:(s : Set α) → MeasurableSet s → ProphC:∀ t ∈ C, ∀ (ht : MeasurableSet t), p t htempty:p ∅ ⋯compl:∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯iUnion:∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ i, s i) ⋯s:Set αt:Set αht:t ∈ Chs:MeasurableSet t⊢ p t hs exact hC t ht hsAll goals completed! 🐙
  | empty =>emptyα:Type u_1inst✝:MeasurableSpace αC:Set (Set α)h_eq:inst✝ = generateFrom Cp:(s : Set α) → MeasurableSet s → ProphC:∀ t ∈ C, ∀ (ht : MeasurableSet t), p t htempty:p ∅ ⋯compl:∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯iUnion:∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ i, s i) ⋯s:Set αhs:MeasurableSet ∅⊢ p ∅ hs exact emptyAll goals completed! 🐙
  | compl t ht ih =>complα:Type u_1inst✝:MeasurableSpace αC:Set (Set α)h_eq:inst✝ = generateFrom Cp:(s : Set α) → MeasurableSet s → ProphC:∀ t ∈ C, ∀ (ht : MeasurableSet t), p t htempty:p ∅ ⋯compl:∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯iUnion:∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ i, s i) ⋯s:Set αt:Set αht:GenerateMeasurable C tih:∀ (hs : MeasurableSet t), p t hshs:MeasurableSet tᶜ⊢ p tᶜ hs exact compl t (h_eq ▸ ht) (ih (h_eq ▸ ht))All goals completed! 🐙
  | iUnion f hf ih =>iUnionα:Type u_1inst✝:MeasurableSpace αC:Set (Set α)h_eq:inst✝ = generateFrom Cp:(s : Set α) → MeasurableSet s → ProphC:∀ t ∈ C, ∀ (ht : MeasurableSet t), p t htempty:p ∅ ⋯compl:∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯iUnion:∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ i, s i) ⋯s:Set αf:ℕ → Set αhf:∀ (n : ℕ), GenerateMeasurable C (f n)ih:∀ (n : ℕ) (hs : MeasurableSet (f n)), p (f n) hshs:MeasurableSet (⋃ i, f i)⊢ p (⋃ i, f i) hs exact iUnion f (h_eq ▸ hf) (fun n ↦ ih n (h_eq ▸ hf n))All goals completed! 🐙

Definition.

Let X be a set, and let \mathcal{F} \subseteq \mathcal{P}(X). We inductively define the set of sets \dgen (\mathcal{F}) \subseteq \mathcal{P}(X), called the Dynkin system generated by \mathcal{F}, as follows:

For any A \in \mathcal{F}, we have A \in \dgen (\mathcal{F}).
\emptyset \in \dgen (\mathcal{F}).
For any A \in \dgen (\mathcal{F}), we have A^c \in \dgen (\mathcal{F}).
For any sequence A_0, A_1, \dots \in \dgen (\mathcal{F}) such that A_i \cap A_j = \emptyset if i \neq j, we have \bigcup_{n \in \mathbb{N}} A_n \in \dgen (\mathcal{F}).

Lean code

inductive GenDynkin (𝓕 : Set (Set X)) : Set (Set X)
  | basic : ∀ A ∈ 𝓕, GenDynkin 𝓕 A
  | empty : GenDynkin 𝓕 ∅
  | compl : ∀ {a}, GenDynkin 𝓕 a → GenDynkin 𝓕 aᶜ
  | iUnion_nat : ∀ {A : ℕ → Set X},
    Pairwise (Disjoint on A) → (∀ i, GenDynkin 𝓕 (A i)) → GenDynkin 𝓕 (⋃ i, A i)

Lemma (Dynkin's π-λ Theorem).

Let X be a measurable space, and let \mathcal{F} \subseteq \mathcal{P}(X). Suppose that \mathcal{M}(X) = \gen (\mathcal{F}). Suppose that for any A, B \in \mathcal{F}, we have A \cap B \in \mathcal{F}. Then for any A \subseteq X, A is measurable if and only if A \in \dgen (\mathcal{F}).

Lean code

@[grind .]
theorem genDynkin_inter_compl_right {𝓕 : Set (Set X)} {A B : Set X}
  (hA : A ∈ GenDynkin 𝓕) (hAB : A ∩ B ∈ GenDynkin 𝓕) :
    A ∩ Bᶜ ∈ GenDynkin 𝓕 := byX:Type u_1𝓕:Set (Set X)A:Set XB:Set XhA:A ∈ GenDynkin 𝓕hAB:A ∩ B ∈ GenDynkin 𝓕⊢ A ∩ Bᶜ ∈ GenDynkin 𝓕
  have : A ∩ Bᶜ = (Aᶜ ∪ (A ∩ B))ᶜ := byX:Type u_1𝓕:Set (Set X)A:Set XB:Set XhA:A ∈ GenDynkin 𝓕hAB:A ∩ B ∈ GenDynkin 𝓕⊢ A ∩ Bᶜ ∈ GenDynkin 𝓕 grindAll goals completed! 🐙
  grindAll goals completed! 🐙

@[grind .]
theorem genDynkin_inter_compl_left {𝓕 : Set (Set X)} {A B : Set X}
  (hB : B ∈ GenDynkin 𝓕) (hAB : A ∩ B ∈ GenDynkin 𝓕) :
    Aᶜ ∩ B ∈ GenDynkin 𝓕 := byX:Type u_1𝓕:Set (Set X)A:Set XB:Set XhB:B ∈ GenDynkin 𝓕hAB:A ∩ B ∈ GenDynkin 𝓕⊢ Aᶜ ∩ B ∈ GenDynkin 𝓕
  rw [inter_comm]X:Type u_1𝓕:Set (Set X)A:Set XB:Set XhB:B ∈ GenDynkin 𝓕hAB:A ∩ B ∈ GenDynkin 𝓕⊢ B ∩ Aᶜ ∈ GenDynkin 𝓕
  grindAll goals completed! 🐙

theorem genDynkin_inter {𝓕 : Set (Set X)} (h𝓕 : ∀ ⦃A B⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕)
    {A B : Set X} (hA : A ∈ GenDynkin 𝓕) (hB : B ∈ GenDynkin 𝓕) : A ∩ B ∈ GenDynkin 𝓕 := byX:Type u_1𝓕:Set (Set X)h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set XB:Set XhA:A ∈ GenDynkin 𝓕hB:B ∈ GenDynkin 𝓕⊢ A ∩ B ∈ GenDynkin 𝓕
  induction hA with
  | basic A hA =>basicX:Type u_1𝓕:Set (Set X)h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A✝:Set XB:Set XhB:B ∈ GenDynkin 𝓕A:Set XhA:A ∈ 𝓕⊢ A ∩ B ∈ GenDynkin 𝓕
    induction hB with
    | basic B hB =>basic.basicX:Type u_1𝓕:Set (Set X)h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A✝:Set XB✝:Set XA:Set XhA:A ∈ 𝓕B:Set XhB:B ∈ 𝓕⊢ A ∩ B ∈ GenDynkin 𝓕 exact genDynkin_basic (h𝓕 hA hB)All goals completed! 🐙
    | empty =>basic.emptyX:Type u_1𝓕:Set (Set X)h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A✝:Set XB:Set XA:Set XhA:A ∈ 𝓕⊢ A ∩ ∅ ∈ GenDynkin 𝓕 simpAll goals completed! 🐙
    | @compl B hB ih =>basic.complX:Type u_1𝓕:Set (Set X)h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A✝:Set XB✝:Set XA:Set XhA:A ∈ 𝓕B:Set XhB:GenDynkin 𝓕 Bih:A ∩ B ∈ GenDynkin 𝓕⊢ A ∩ Bᶜ ∈ GenDynkin 𝓕 grindAll goals completed! 🐙
    | @iUnion_nat f hdf hf ih =>basic.iUnion_natX:Type u_1𝓕:Set (Set X)h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A✝:Set XB:Set XA:Set XhA:A ∈ 𝓕f:ℕ → Set Xhdf:Pairwise (Disjoint on f)hf:∀ (i : ℕ), GenDynkin 𝓕 (f i)ih:∀ (i : ℕ), A ∩ f i ∈ GenDynkin 𝓕⊢ A ∩ ⋃ i, f i ∈ GenDynkin 𝓕
      simpa [inter_iUnion] using genDynkin_iUnion (pairwise_disjoint_inter_left hdf A) ihAll goals completed! 🐙
  | empty =>emptyX:Type u_1𝓕:Set (Set X)h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set XB:Set XhB:B ∈ GenDynkin 𝓕⊢ ∅ ∩ B ∈ GenDynkin 𝓕 simpAll goals completed! 🐙
  | @compl A hA ih =>complX:Type u_1𝓕:Set (Set X)h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A✝:Set XB:Set XhB:B ∈ GenDynkin 𝓕A:Set XhA:GenDynkin 𝓕 Aih:A ∩ B ∈ GenDynkin 𝓕⊢ Aᶜ ∩ B ∈ GenDynkin 𝓕 grindAll goals completed! 🐙
  | @iUnion_nat f hdf hf ih =>iUnion_natX:Type u_1𝓕:Set (Set X)h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set XB:Set XhB:B ∈ GenDynkin 𝓕f:ℕ → Set Xhdf:Pairwise (Disjoint on f)hf:∀ (i : ℕ), GenDynkin 𝓕 (f i)ih:∀ (i : ℕ), f i ∩ B ∈ GenDynkin 𝓕⊢ (⋃ i, f i) ∩ B ∈ GenDynkin 𝓕
    simpa [iUnion_inter] using genDynkin_iUnion (pairwise_disjoint_inter_right hdf B) ihAll goals completed! 🐙

theorem measurableSet_iff_mem_genDynkin [MeasurableSpace X] {𝓕 : Set (Set X)}
    (h : ‹_› = generateFrom 𝓕) (h𝓕 : ∀ ⦃A B⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕) (A : Set X) :
    MeasurableSet A ↔ A ∈ GenDynkin 𝓕 := byX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set X⊢ MeasurableSet A ↔ A ∈ GenDynkin 𝓕
  apply Iff.intrompX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set X⊢ MeasurableSet A → A ∈ GenDynkin 𝓕mprX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set X⊢ A ∈ GenDynkin 𝓕 → MeasurableSet A
  ·mpX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set X⊢ MeasurableSet A → A ∈ GenDynkin 𝓕 intro hAmpX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set XhA:MeasurableSet A⊢ A ∈ GenDynkin 𝓕
    rw [h] at hAmpX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set XhA:MeasurableSet A⊢ A ∈ GenDynkin 𝓕
    induction hA with
    | basic A hA =>mp.basicX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A✝:Set XA:Set XhA:A ∈ 𝓕⊢ A ∈ GenDynkin 𝓕 grindAll goals completed! 🐙
    | empty =>mp.emptyX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set X⊢ ∅ ∈ GenDynkin 𝓕 grindAll goals completed! 🐙
    | @compl A hA ih =>mp.complX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A✝:Set XA:Set XhA:GenerateMeasurable 𝓕 Aih:A ∈ GenDynkin 𝓕⊢ Aᶜ ∈ GenDynkin 𝓕 grindAll goals completed! 🐙
    | @iUnion f hf ih =>mp.iUnionX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set Xf:ℕ → Set Xhf:∀ (n : ℕ), GenerateMeasurable 𝓕 (f n)ih:∀ (n : ℕ), f n ∈ GenDynkin 𝓕⊢ ⋃ i, f i ∈ GenDynkin 𝓕
      rw [← iUnion_disjointed]mp.iUnionX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set Xf:ℕ → Set Xhf:∀ (n : ℕ), GenerateMeasurable 𝓕 (f n)ih:∀ (n : ℕ), f n ∈ GenDynkin 𝓕⊢ ⋃ i, disjointed f i ∈ GenDynkin 𝓕
      apply genDynkin_iUnion (disjoint_disjointed f)mp.iUnionX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set Xf:ℕ → Set Xhf:∀ (n : ℕ), GenerateMeasurable 𝓕 (f n)ih:∀ (n : ℕ), f n ∈ GenDynkin 𝓕⊢ ∀ (i : ℕ), disjointed f i ∈ GenDynkin 𝓕
      intro nmp.iUnionX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set Xf:ℕ → Set Xhf:∀ (n : ℕ), GenerateMeasurable 𝓕 (f n)ih:∀ (n : ℕ), f n ∈ GenDynkin 𝓕n:ℕ⊢ disjointed f n ∈ GenDynkin 𝓕
      apply disjointedRec _ (ih n)X:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set Xf:ℕ → Set Xhf:∀ (n : ℕ), GenerateMeasurable 𝓕 (f n)ih:∀ (n : ℕ), f n ∈ GenDynkin 𝓕n:ℕ⊢ ∀ ⦃t : Set X⦄ ⦃i : ℕ⦄, t ∈ GenDynkin 𝓕 → t \ f i ∈ GenDynkin 𝓕
      intro A nX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A✝:Set Xf:ℕ → Set Xhf:∀ (n : ℕ), GenerateMeasurable 𝓕 (f n)ih:∀ (n : ℕ), f n ∈ GenDynkin 𝓕n✝:ℕA:Set Xn:ℕ⊢ A ∈ GenDynkin 𝓕 → A \ f n ∈ GenDynkin 𝓕 hAX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A✝:Set Xf:ℕ → Set Xhf:∀ (n : ℕ), GenerateMeasurable 𝓕 (f n)ih:∀ (n : ℕ), f n ∈ GenDynkin 𝓕n✝:ℕA:Set Xn:ℕhA:A ∈ GenDynkin 𝓕⊢ A \ f n ∈ GenDynkin 𝓕
      rw [@diff_eq]X:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A✝:Set Xf:ℕ → Set Xhf:∀ (n : ℕ), GenerateMeasurable 𝓕 (f n)ih:∀ (n : ℕ), f n ∈ GenDynkin 𝓕n✝:ℕA:Set Xn:ℕhA:A ∈ GenDynkin 𝓕⊢ A ∩ (f n)ᶜ ∈ GenDynkin 𝓕
      apply genDynkin_inter h𝓕 hA (genDynkin_compl (ih n))All goals completed! 🐙
  ·mprX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set X⊢ A ∈ GenDynkin 𝓕 → MeasurableSet A intro hAmprX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set XhA:A ∈ GenDynkin 𝓕⊢ MeasurableSet A
    induction hA with
    | basic A hA =>mpr.basicX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A✝:Set XA:Set XhA:A ∈ 𝓕⊢ MeasurableSet A apply h ▸ measurableSet_generateFrom hAAll goals completed! 🐙
    | empty =>mpr.emptyX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set X⊢ MeasurableSet ∅ apply MeasurableSet.emptyAll goals completed! 🐙
    | @compl A hA ih =>mpr.complX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A✝:Set XA:Set XhA:GenDynkin 𝓕 Aih:MeasurableSet A⊢ MeasurableSet Aᶜ apply MeasurableSet.compl ihAll goals completed! 🐙
    | @iUnion_nat f hdf hf ih =>mpr.iUnion_natX:Type u_1inst✝:MeasurableSpace X𝓕:Set (Set X)h:inst✝ = generateFrom 𝓕h𝓕:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕A:Set Xf:ℕ → Set Xhdf:Pairwise (Disjoint on f)hf:∀ (i : ℕ), GenDynkin 𝓕 (f i)ih:∀ (i : ℕ), MeasurableSet (f i)⊢ MeasurableSet (⋃ i, f i) apply MeasurableSet.iUnion ihAll goals completed! 🐙

Lemma (Induction Principle for Measurable Sets after π-λ).

Let X be a measurable space, and let \mathcal{F} \subseteq \mathcal{P}(X). Suppose that \mathcal{M}(X) = \gen (\mathcal{F}). Suppose that for any A, B \in \mathcal{F}, we have A \cap B \in \mathcal{F}. Let P(A) be a property on measurable sets A \subseteq X. Suppose that the following conditions hold:

For any A \in \mathcal{F}, we have P(A).
We have P(\emptyset).
For any measurable set A \subseteq X, we have P(A) implies P(A^c).
For any sequence of measurable sets A_0, A_1, \dots \subseteq X such that A_i \cap A_j = \emptyset if i \neq j, we have \forall n \in \mathbb{N}, P(A_n) implies P\left(\bigcup_{n \in \mathbb{N}} A_n\right).

Then any measurable set A \subseteq X satisfies P(A).

Lean code

@[elab_as_elim]
theorem induction_on_inter
    [m : MeasurableSpace X] {P : ∀ A : Set X, MeasurableSet A → Prop}
    {𝓕 : Set (Set X)} (h_eq : m = generateFrom 𝓕) (h_inter : ∀ ⦃A B⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕)
    (empty : P ∅ .empty)
    (basic : ∀ A (hA : A ∈ 𝓕), P A <| h_eq ▸ measurableSet_generateFrom hA)
    (compl : ∀ A (hAm : MeasurableSet A), P A hAm → P Aᶜ hAm.compl)
    (iUnion : ∀ (A : ℕ → Set X), Pairwise (Disjoint on A) → ∀ (hAm : ∀ i, MeasurableSet (A i)),
      (∀ i, P (A i) (hAm i)) → P (⋃ i, A i) (.iUnion hAm))
    (A : Set X) (hA : MeasurableSet A) :
    P A hA := byX:Type u_1m:MeasurableSpace XP:(A : Set X) → MeasurableSet A → Prop𝓕:Set (Set X)h_eq:m = generateFrom 𝓕h_inter:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕empty:P ∅ ⋯basic:∀ (A : Set X) (hA : A ∈ 𝓕), P A ⋯compl:∀ (A : Set X) (hAm : MeasurableSet A), P A hAm → P Aᶜ ⋯iUnion:∀ (A : ℕ → Set X),
  Pairwise (Disjoint on A) → ∀ (hAm : ∀ (i : ℕ), MeasurableSet (A i)), (∀ (i : ℕ), P (A i) ⋯) → P (⋃ i, A i) ⋯A:Set XhA:MeasurableSet A⊢ P A hA
  have hA' := (measurableSet_iff_mem_genDynkin h_eq h_inter A).mp hAX:Type u_1m:MeasurableSpace XP:(A : Set X) → MeasurableSet A → Prop𝓕:Set (Set X)h_eq:m = generateFrom 𝓕h_inter:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕empty:P ∅ ⋯basic:∀ (A : Set X) (hA : A ∈ 𝓕), P A ⋯compl:∀ (A : Set X) (hAm : MeasurableSet A), P A hAm → P Aᶜ ⋯iUnion:∀ (A : ℕ → Set X),
  Pairwise (Disjoint on A) → ∀ (hAm : ∀ (i : ℕ), MeasurableSet (A i)), (∀ (i : ℕ), P (A i) ⋯) → P (⋃ i, A i) ⋯A:Set XhA:MeasurableSet AhA':A ∈ GenDynkin 𝓕 := (measurableSet_iff_mem_genDynkin h_eq h_inter A).mp hA⊢ P A hA
  induction hA' using GenDynkin.rec with
  | basic A hA' =>basicX:Type u_1m:MeasurableSpace XP:(A : Set X) → MeasurableSet A → Prop𝓕:Set (Set X)h_eq:m = generateFrom 𝓕h_inter:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕empty:P ∅ ⋯basic:∀ (A : Set X) (hA : A ∈ 𝓕), P A ⋯compl:∀ (A : Set X) (hAm : MeasurableSet A), P A hAm → P Aᶜ ⋯iUnion:∀ (A : ℕ → Set X),
  Pairwise (Disjoint on A) → ∀ (hAm : ∀ (i : ℕ), MeasurableSet (A i)), (∀ (i : ℕ), P (A i) ⋯) → P (⋃ i, A i) ⋯A✝:Set XA:Set XhA':A ∈ 𝓕hA:MeasurableSet A⊢ P A hA exact basic A hA'All goals completed! 🐙
  | empty =>emptyX:Type u_1m:MeasurableSpace XP:(A : Set X) → MeasurableSet A → Prop𝓕:Set (Set X)h_eq:m = generateFrom 𝓕h_inter:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕empty:P ∅ ⋯basic:∀ (A : Set X) (hA : A ∈ 𝓕), P A ⋯compl:∀ (A : Set X) (hAm : MeasurableSet A), P A hAm → P Aᶜ ⋯iUnion:∀ (A : ℕ → Set X),
  Pairwise (Disjoint on A) → ∀ (hAm : ∀ (i : ℕ), MeasurableSet (A i)), (∀ (i : ℕ), P (A i) ⋯) → P (⋃ i, A i) ⋯A:Set XhA:MeasurableSet ∅⊢ P ∅ hA exact emptyAll goals completed! 🐙
  | @compl A hA' ih =>complX:Type u_1m:MeasurableSpace XP:(A : Set X) → MeasurableSet A → Prop𝓕:Set (Set X)h_eq:m = generateFrom 𝓕h_inter:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕empty:P ∅ ⋯basic:∀ (A : Set X) (hA : A ∈ 𝓕), P A ⋯compl:∀ (A : Set X) (hAm : MeasurableSet A), P A hAm → P Aᶜ ⋯iUnion:∀ (A : ℕ → Set X),
  Pairwise (Disjoint on A) → ∀ (hAm : ∀ (i : ℕ), MeasurableSet (A i)), (∀ (i : ℕ), P (A i) ⋯) → P (⋃ i, A i) ⋯A✝:Set XA:Set XhA':GenDynkin 𝓕 Aih:∀ (hA : MeasurableSet A), P A hAhA:MeasurableSet Aᶜ⊢ P Aᶜ hA
    apply compl A ((measurableSet_iff_mem_genDynkin h_eq h_inter A).mpr hA') (ih _)All goals completed! 🐙
  | @iUnion_nat A hAd hA' ih =>iUnion_natX:Type u_1m:MeasurableSpace XP:(A : Set X) → MeasurableSet A → Prop𝓕:Set (Set X)h_eq:m = generateFrom 𝓕h_inter:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕empty:P ∅ ⋯basic:∀ (A : Set X) (hA : A ∈ 𝓕), P A ⋯compl:∀ (A : Set X) (hAm : MeasurableSet A), P A hAm → P Aᶜ ⋯iUnion:∀ (A : ℕ → Set X),
  Pairwise (Disjoint on A) → ∀ (hAm : ∀ (i : ℕ), MeasurableSet (A i)), (∀ (i : ℕ), P (A i) ⋯) → P (⋃ i, A i) ⋯A✝:Set XA:ℕ → Set XhAd:Pairwise (Disjoint on A)hA':∀ (i : ℕ), GenDynkin 𝓕 (A i)ih:∀ (i : ℕ) (hA : MeasurableSet (A i)), P (A i) hAhA:MeasurableSet (⋃ i, A i)⊢ P (⋃ i, A i) hA
    apply iUnion _ hAd _ (fun n ↦ ih n _)X:Type u_1m:MeasurableSpace XP:(A : Set X) → MeasurableSet A → Prop𝓕:Set (Set X)h_eq:m = generateFrom 𝓕h_inter:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕empty:P ∅ ⋯basic:∀ (A : Set X) (hA : A ∈ 𝓕), P A ⋯compl:∀ (A : Set X) (hAm : MeasurableSet A), P A hAm → P Aᶜ ⋯iUnion:∀ (A : ℕ → Set X),
  Pairwise (Disjoint on A) → ∀ (hAm : ∀ (i : ℕ), MeasurableSet (A i)), (∀ (i : ℕ), P (A i) ⋯) → P (⋃ i, A i) ⋯A✝:Set XA:ℕ → Set XhAd:Pairwise (Disjoint on A)hA':∀ (i : ℕ), GenDynkin 𝓕 (A i)ih:∀ (i : ℕ) (hA : MeasurableSet (A i)), P (A i) hAhA:MeasurableSet (⋃ i, A i)⊢ ∀ (i : ℕ), MeasurableSet (A i)
    intro nX:Type u_1m:MeasurableSpace XP:(A : Set X) → MeasurableSet A → Prop𝓕:Set (Set X)h_eq:m = generateFrom 𝓕h_inter:∀ ⦃A B : Set X⦄, A ∈ 𝓕 → B ∈ 𝓕 → A ∩ B ∈ 𝓕empty:P ∅ ⋯basic:∀ (A : Set X) (hA : A ∈ 𝓕), P A ⋯compl:∀ (A : Set X) (hAm : MeasurableSet A), P A hAm → P Aᶜ ⋯iUnion:∀ (A : ℕ → Set X),
  Pairwise (Disjoint on A) → ∀ (hAm : ∀ (i : ℕ), MeasurableSet (A i)), (∀ (i : ℕ), P (A i) ⋯) → P (⋃ i, A i) ⋯A✝:Set XA:ℕ → Set XhAd:Pairwise (Disjoint on A)hA':∀ (i : ℕ), GenDynkin 𝓕 (A i)ih:∀ (i : ℕ) (hA : MeasurableSet (A i)), P (A i) hAhA:MeasurableSet (⋃ i, A i)n:ℕ⊢ MeasurableSet (A n)
    apply (measurableSet_iff_mem_genDynkin h_eq h_inter (A n)).mpr (hA' n)All goals completed! 🐙