Induction principles for measurable sets, related to π-systems and λ-systems.

Main statements

• The main theorem of this file is Dynkin's π-λ theorem, which appears here as an induction principle induction_on_inter. Suppose s is a collection of subsets of α such that the intersection of two members of s belongs to s whenever it is nonempty. Let m be the σ-algebra generated by s. In order to check that a predicate C holds on every member of m, it suffices to check that C holds on the members of s and that C is preserved by complementation and disjoint countable unions.

• The proof of this theorem relies on the notion of IsPiSystem, i.e., a collection of sets which is closed under binary non-empty intersections. Note that this is a small variation around the usual notion in the literature, which often requires that a π-system is non-empty, and closed also under disjoint intersections. This variation turns out to be convenient for the formalization.

• The proof of Dynkin's π-λ theorem also requires the notion of DynkinSystem, i.e., a collection of sets which contains the empty set, is closed under complementation and under countable union of pairwise disjoint sets. The disjointness condition is the only difference with σ-algebras.

• generatePiSystem g gives the minimal π-system containing g. This can be considered a Galois insertion into both measurable spaces and sets.

• generateFrom_generatePiSystem_eq proves that if you start from a collection of sets g, take the generated π-system, and then the generated σ-algebra, you get the same result as the σ-algebra generated from g. This is useful because there are connections between independent sets that are π-systems and the generated independent spaces.

• mem_generatePiSystem_iUnion_elim and mem_generatePiSystem_iUnion_elim' show that any element of the π-system generated from the union of a set of π-systems can be represented as the intersection of a finite number of elements from these sets.

• piiUnionInter defines a new π-system from a family of π-systems π : ι → Set (Set α) and a set of indices S : Set ι. piiUnionInter π S is the set of sets that can be written as ⋂ x ∈ t, f x for some finset t ∈ S and sets f x ∈ π x.

Implementation details

• IsPiSystem is a predicate, not a type. Thus, we don't explicitly define the galois insertion, nor do we define a complete lattice. In theory, we could define a complete lattice and galois insertion on the subtype corresponding to IsPiSystem.

def IsPiSystem {α : Type u_1} (C : Set (Set α)) : Prop

A π-system is a collection of subsets of α that is closed under binary intersection of non-disjoint sets. Usually it is also required that the collection is nonempty, but we don't do that here.

Equations

• IsPiSystem C = ∀ s ∈ C, ∀ t ∈ C, (s ∩ t).Nonempty → s ∩ t ∈ C

theorem MeasurableSpace.isPiSystem_measurableSet {α : Type u_3} [MeasurableSpace α] : IsPiSystem {s : Set α | MeasurableSet s}

theorem IsPiSystem.singleton {α : Type u_1} (S : Set α) : IsPiSystem {S}

theorem IsPiSystem.insert_empty {α : Type u_1} {S : Set (Set α)} (h_pi : IsPiSystem S) : IsPiSystem (insert ∅ S)

theorem IsPiSystem.insert_univ {α : Type u_1} {S : Set (Set α)} (h_pi : IsPiSystem S) : IsPiSystem (insert Set.univ S)

theorem IsPiSystem.comap {α : Type u_3} {β : Type u_4} {S : Set (Set β)} (h_pi : IsPiSystem S) (f : α → β) : IsPiSystem {s : Set α | ∃ t ∈ S, f ⁻¹' t = s}

theorem isPiSystem_iUnion_of_directed_le {α : Type u_3} {ι : Sort u_4} (p : ι → Set (Set α)) (hp_pi : ∀ (n : ι), IsPiSystem (p n)) (hp_directed : Directed (fun (x1 x2 : Set (Set α)) => x1 ≤ x2) p) : IsPiSystem (⋃ (n : ι), p n)

theorem isPiSystem_iUnion_of_monotone {α : Type u_3} {ι : Type u_4} [SemilatticeSup ι] (p : ι → Set (Set α)) (hp_pi : ∀ (n : ι), IsPiSystem (p n)) (hp_mono : Monotone p) : IsPiSystem (⋃ (n : ι), p n)

theorem IsPiSystem.prod {α : Type u_1} {β : Type u_2} {C : Set (Set α)} {D : Set (Set β)} (hC : IsPiSystem C) (hD : IsPiSystem D) : IsPiSystem (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) C D)

Rectangles formed by π-systems form a π-system.

theorem isPiSystem_image_Iio {α : Type u_1} [LinearOrder α] (s : Set α) : IsPiSystem (Set.Iio '' s)

theorem isPiSystem_Iio {α : Type u_1} [LinearOrder α] : IsPiSystem (Set.range Set.Iio)

theorem isPiSystem_image_Ioi {α : Type u_1} [LinearOrder α] (s : Set α) : IsPiSystem (Set.Ioi '' s)

theorem isPiSystem_Ioi {α : Type u_1} [LinearOrder α] : IsPiSystem (Set.range Set.Ioi)

theorem isPiSystem_image_Iic {α : Type u_1} [LinearOrder α] (s : Set α) : IsPiSystem (Set.Iic '' s)

theorem isPiSystem_Iic {α : Type u_1} [LinearOrder α] : IsPiSystem (Set.range Set.Iic)

theorem isPiSystem_image_Ici {α : Type u_1} [LinearOrder α] (s : Set α) : IsPiSystem (Set.Ici '' s)

theorem isPiSystem_Ici {α : Type u_1} [LinearOrder α] : IsPiSystem (Set.range Set.Ici)

theorem isPiSystem_Ixx_mem {α : Type u_1} [LinearOrder α] {Ixx : α → α → Set α} {p : α → α → Prop} (Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b) (Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (a₁ ⊔ a₂) (b₁ ⊓ b₂)) (s : Set α) (t : Set α) : IsPiSystem {S : Set α | ∃ l ∈ s, ∃ u ∈ t, p l u ∧ Ixx l u = S}

theorem isPiSystem_Ixx {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} [LinearOrder α] {Ixx : α → α → Set α} {p : α → α → Prop} (Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b) (Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (a₁ ⊔ a₂) (b₁ ⊓ b₂)) (f : ι → α) (g : ι' → α) : IsPiSystem {S : Set α | ∃ (i : ι) (j : ι'), p (f i) (g j) ∧ Ixx (f i) (g j) = S}

theorem isPiSystem_Ioo_mem {α : Type u_1} [LinearOrder α] (s : Set α) (t : Set α) : IsPiSystem {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Set.Ioo l u = S}

theorem isPiSystem_Ioo {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} [LinearOrder α] (f : ι → α) (g : ι' → α) : IsPiSystem {S : Set α | ∃ (l : ι) (u : ι'), f l < g u ∧ Set.Ioo (f l) (g u) = S}

theorem isPiSystem_Ioc_mem {α : Type u_1} [LinearOrder α] (s : Set α) (t : Set α) : IsPiSystem {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Set.Ioc l u = S}

theorem isPiSystem_Ioc {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} [LinearOrder α] (f : ι → α) (g : ι' → α) : IsPiSystem {S : Set α | ∃ (i : ι) (j : ι'), f i < g j ∧ Set.Ioc (f i) (g j) = S}

theorem isPiSystem_Ico_mem {α : Type u_1} [LinearOrder α] (s : Set α) (t : Set α) : IsPiSystem {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Set.Ico l u = S}

theorem isPiSystem_Ico {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} [LinearOrder α] (f : ι → α) (g : ι' → α) : IsPiSystem {S : Set α | ∃ (i : ι) (j : ι'), f i < g j ∧ Set.Ico (f i) (g j) = S}

theorem isPiSystem_Icc_mem {α : Type u_1} [LinearOrder α] (s : Set α) (t : Set α) : IsPiSystem {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l ≤ u ∧ Set.Icc l u = S}

theorem isPiSystem_Icc {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} [LinearOrder α] (f : ι → α) (g : ι' → α) : IsPiSystem {S : Set α | ∃ (i : ι) (j : ι'), f i ≤ g j ∧ Set.Icc (f i) (g j) = S}

inductive generatePiSystem {α : Type u_1} (S : Set (Set α)) : Set (Set α)

Given a collection S of subsets of α, then generatePiSystem S is the smallest π-system containing S.

• base: ∀ {α : Type u_1} {S : Set (Set α)} {s : Set α}, s ∈ S → generatePiSystem S s
• inter: ∀ {α : Type u_1} {S : Set (Set α)} {s t : Set α}, generatePiSystem S s → generatePiSystem S t → (s ∩ t).Nonempty → generatePiSystem S (s ∩ t)

theorem isPiSystem_generatePiSystem {α : Type u_1} (S : Set (Set α)) : IsPiSystem (generatePiSystem S)

theorem subset_generatePiSystem_self {α : Type u_1} (S : Set (Set α)) : S ⊆ generatePiSystem S

theorem generatePiSystem_subset_self {α : Type u_1} {S : Set (Set α)} (h_S : IsPiSystem S) : generatePiSystem S ⊆ S

theorem generatePiSystem_eq {α : Type u_1} {S : Set (Set α)} (h_pi : IsPiSystem S) : generatePiSystem S = S

theorem generatePiSystem_mono {α : Type u_1} {S : Set (Set α)} {T : Set (Set α)} (hST : S ⊆ T) : generatePiSystem S ⊆ generatePiSystem T

theorem generatePiSystem_measurableSet {α : Type u_1} [M : MeasurableSpace α] {S : Set (Set α)} (h_meas_S : ∀ s ∈ S, MeasurableSet s) (t : Set α) (h_in_pi : t ∈ generatePiSystem S) : MeasurableSet t

theorem generateFrom_measurableSet_of_generatePiSystem {α : Type u_1} {g : Set (Set α)} (t : Set α) (ht : t ∈ generatePiSystem g) : MeasurableSet t

theorem generateFrom_generatePiSystem_eq {α : Type u_1} {g : Set (Set α)} : MeasurableSpace.generateFrom (generatePiSystem g) = MeasurableSpace.generateFrom g

theorem mem_generatePiSystem_iUnion_elim {α : Type u_3} {β : Type u_4} {g : β → Set (Set α)} (h_pi : ∀ (b : β), IsPiSystem (g b)) (t : Set α) (h_t : t ∈ generatePiSystem (⋃ (b : β), g b)) : ∃ (T : Finset β) (f : β → Set α), t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Every element of the π-system generated by the union of a family of π-systems is a finite intersection of elements from the π-systems. For an indexed union version, see mem_generatePiSystem_iUnion_elim'.

theorem mem_generatePiSystem_iUnion_elim' {α : Type u_3} {β : Type u_4} {g : β → Set (Set α)} {s : Set β} (h_pi : ∀ b ∈ s, IsPiSystem (g b)) (t : Set α) (h_t : t ∈ generatePiSystem (⋃ b ∈ s, g b)) : ∃ (T : Finset β) (f : β → Set α), ↑T ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Every element of the π-system generated by an indexed union of a family of π-systems is a finite intersection of elements from the π-systems. For a total union version, see mem_generatePiSystem_iUnion_elim.

π-system generated by finite intersections of sets of a π-system family

def piiUnionInter {α : Type u_3} {ι : Type u_4} (π : ι → Set (Set α)) (S : Set ι) : Set (Set α)

From a set of indices S : Set ι and a family of sets of sets π : ι → Set (Set α), define the set of sets that can be written as ⋂ x ∈ t, f x for some finset t ⊆ S and sets f x ∈ π x. If π is a family of π-systems, then it is a π-system.

Equations

• piiUnionInter π S = {s : Set α | ∃ (t : Finset ι) (_ : ↑t ⊆ S) (f : ι → Set α) (_ : ∀ x ∈ t, f x ∈ π x), s = ⋂ x ∈ t, f x}

theorem piiUnionInter_singleton {α : Type u_3} {ι : Type u_4} (π : ι → Set (Set α)) (i : ι) : piiUnionInter π {i} = π i ∪ {Set.univ}

theorem piiUnionInter_singleton_left {α : Type u_3} {ι : Type u_4} (s : ι → Set α) (S : Set ι) : piiUnionInter (fun (i : ι) => {s i}) S = {s' : Set α | ∃ (t : Finset ι) (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i}

theorem generateFrom_piiUnionInter_singleton_left {α : Type u_3} {ι : Type u_4} (s : ι → Set α) (S : Set ι) : MeasurableSpace.generateFrom (piiUnionInter (fun (k : ι) => {s k}) S) = MeasurableSpace.generateFrom {t : Set α | ∃ k ∈ S, s k = t}

theorem isPiSystem_piiUnionInter {α : Type u_3} {ι : Type u_4} (π : ι → Set (Set α)) (hpi : ∀ (x : ι), IsPiSystem (π x)) (S : Set ι) : IsPiSystem (piiUnionInter π S)

If π is a family of π-systems, then piiUnionInter π S is a π-system.

theorem piiUnionInter_mono_left {α : Type u_3} {ι : Type u_4} {π : ι → Set (Set α)} {π' : ι → Set (Set α)} (h_le : ∀ (i : ι), π i ⊆ π' i) (S : Set ι) : piiUnionInter π S ⊆ piiUnionInter π' S

theorem piiUnionInter_mono_right {α : Type u_3} {ι : Type u_4} {π : ι → Set (Set α)} {S : Set ι} {T : Set ι} (hST : S ⊆ T) : piiUnionInter π S ⊆ piiUnionInter π T

theorem generateFrom_piiUnionInter_le {α : Type u_3} {ι : Type u_4} {m : MeasurableSpace α} (π : ι → Set (Set α)) (h : ∀ (n : ι), MeasurableSpace.generateFrom (π n) ≤ m) (S : Set ι) : MeasurableSpace.generateFrom (piiUnionInter π S) ≤ m

theorem subset_piiUnionInter {α : Type u_3} {ι : Type u_4} {π : ι → Set (Set α)} {S : Set ι} {i : ι} (his : i ∈ S) : π i ⊆ piiUnionInter π S

theorem mem_piiUnionInter_of_measurableSet {α : Type u_3} {ι : Type u_4} (m : ι → MeasurableSpace α) {S : Set ι} {i : ι} (hiS : i ∈ S) (s : Set α) (hs : MeasurableSet s) : s ∈ piiUnionInter (fun (n : ι) => {s : Set α | MeasurableSet s}) S

theorem le_generateFrom_piiUnionInter {α : Type u_3} {ι : Type u_4} {π : ι → Set (Set α)} (S : Set ι) {x : ι} (hxS : x ∈ S) : MeasurableSpace.generateFrom (π x) ≤ MeasurableSpace.generateFrom (piiUnionInter π S)

theorem measurableSet_iSup_of_mem_piiUnionInter {α : Type u_3} {ι : Type u_4} (m : ι → MeasurableSpace α) (S : Set ι) (t : Set α) (ht : t ∈ piiUnionInter (fun (n : ι) => {s : Set α | MeasurableSet s}) S) : MeasurableSet t

theorem generateFrom_piiUnionInter_measurableSet {α : Type u_3} {ι : Type u_4} (m : ι → MeasurableSpace α) (S : Set ι) : MeasurableSpace.generateFrom (piiUnionInter (fun (n : ι) => {s : Set α | MeasurableSet s}) S) = ⨆ i ∈ S, m i

Dynkin systems and Π-λ theorem

structure MeasurableSpace.DynkinSystem (α : Type u_4) : Type u_4

A Dynkin system is a collection of subsets of a type α that contains the empty set, is closed under complementation and under countable union of pairwise disjoint sets. The disjointness condition is the only difference with σ-algebras.

The main purpose of Dynkin systems is to provide a powerful induction rule for σ-algebras generated by a collection of sets which is stable under intersection.

A Dynkin system is also known as a "λ-system" or a "d-system".

• Has : Set α → Prop

  Predicate saying that a given set is contained in the Dynkin system.

• has_empty : self.Has ∅

  A Dynkin system contains the empty set.

• has_compl : ∀ {a : Set α}, self.Has a → self.Has aᶜ

  A Dynkin system is closed under complementation.

• has_iUnion_nat : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), self.Has (f i)) → self.Has (⋃ (i : ℕ), f i)

  A Dynkin system is closed under countable union of pairwise disjoint sets. Use a more general MeasurableSpace.DynkinSystem.has_iUnion instead.

theorem MeasurableSpace.DynkinSystem.has_empty {α : Type u_4} (self : MeasurableSpace.DynkinSystem α) : self.Has ∅

A Dynkin system contains the empty set.

theorem MeasurableSpace.DynkinSystem.has_compl {α : Type u_4} (self : MeasurableSpace.DynkinSystem α) {a : Set α} : self.Has a → self.Has aᶜ

A Dynkin system is closed under complementation.

theorem MeasurableSpace.DynkinSystem.has_iUnion_nat {α : Type u_4} (self : MeasurableSpace.DynkinSystem α) {f : ℕ → Set α} : Pairwise (Disjoint on f) → (∀ (i : ℕ), self.Has (f i)) → self.Has (⋃ (i : ℕ), f i)

A Dynkin system is closed under countable union of pairwise disjoint sets. Use a more general MeasurableSpace.DynkinSystem.has_iUnion instead.

theorem MeasurableSpace.DynkinSystem.ext {α : Type u_3} {d₁ : MeasurableSpace.DynkinSystem α} {d₂ : MeasurableSpace.DynkinSystem α} : (∀ (s : Set α), d₁.Has s ↔ d₂.Has s) → d₁ = d₂

theorem MeasurableSpace.DynkinSystem.has_compl_iff {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {a : Set α} : d.Has aᶜ ↔ d.Has a

theorem MeasurableSpace.DynkinSystem.has_univ {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) : d.Has Set.univ

theorem MeasurableSpace.DynkinSystem.has_iUnion {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {β : Type u_4} [Countable β] {f : β → Set α} (hd : Pairwise (Disjoint on f)) (h : ∀ (i : β), d.Has (f i)) : d.Has (⋃ (i : β), f i)

theorem MeasurableSpace.DynkinSystem.has_union {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {s₁ : Set α} {s₂ : Set α} (h₁ : d.Has s₁) (h₂ : d.Has s₂) (h : Disjoint s₁ s₂) : d.Has (s₁ ∪ s₂)

theorem MeasurableSpace.DynkinSystem.has_diff {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {s₁ : Set α} {s₂ : Set α} (h₁ : d.Has s₁) (h₂ : d.Has s₂) (h : s₂ ⊆ s₁) : d.Has (s₁ \ s₂)

instance MeasurableSpace.DynkinSystem.instLEDynkinSystem {α : Type u_3} : LE (MeasurableSpace.DynkinSystem α)

Equations

• MeasurableSpace.DynkinSystem.instLEDynkinSystem = { le := fun (m₁ m₂ : MeasurableSpace.DynkinSystem α) => m₁.Has ≤ m₂.Has }

theorem MeasurableSpace.DynkinSystem.le_def {α : Type u_3} {a : MeasurableSpace.DynkinSystem α} {b : MeasurableSpace.DynkinSystem α} : a ≤ b ↔ a.Has ≤ b.Has

instance MeasurableSpace.DynkinSystem.instPartialOrder {α : Type u_3} : PartialOrder (MeasurableSpace.DynkinSystem α)

Equations

• MeasurableSpace.DynkinSystem.instPartialOrder = PartialOrder.mk ⋯

def MeasurableSpace.DynkinSystem.ofMeasurableSpace {α : Type u_3} (m : MeasurableSpace α) : MeasurableSpace.DynkinSystem α

Every measurable space (σ-algebra) forms a Dynkin system

Equations

• MeasurableSpace.DynkinSystem.ofMeasurableSpace m = { Has := m.MeasurableSet', has_empty := ⋯, has_compl := ⋯, has_iUnion_nat := ⋯ }

theorem MeasurableSpace.DynkinSystem.ofMeasurableSpace_le_ofMeasurableSpace_iff {α : Type u_3} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} : MeasurableSpace.DynkinSystem.ofMeasurableSpace m₁ ≤ MeasurableSpace.DynkinSystem.ofMeasurableSpace m₂ ↔ m₁ ≤ m₂

inductive MeasurableSpace.DynkinSystem.GenerateHas {α : Type u_3} (s : Set (Set α)) : Set α → Prop

The least Dynkin system containing a collection of basic sets. This inductive type gives the underlying collection of sets.

• basic: ∀ {α : Type u_3} {s : Set (Set α)}, ∀ t ∈ s, MeasurableSpace.DynkinSystem.GenerateHas s t
• empty: ∀ {α : Type u_3} {s : Set (Set α)}, MeasurableSpace.DynkinSystem.GenerateHas s ∅
• compl: ∀ {α : Type u_3} {s : Set (Set α)} {a : Set α}, MeasurableSpace.DynkinSystem.GenerateHas s a → MeasurableSpace.DynkinSystem.GenerateHas s aᶜ
• iUnion: ∀ {α : Type u_3} {s : Set (Set α)} {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSpace.DynkinSystem.GenerateHas s (f i)) → MeasurableSpace.DynkinSystem.GenerateHas s (⋃ (i : ℕ), f i)

theorem MeasurableSpace.DynkinSystem.generateHas_compl {α : Type u_3} {C : Set (Set α)} {s : Set α} : MeasurableSpace.DynkinSystem.GenerateHas C sᶜ ↔ MeasurableSpace.DynkinSystem.GenerateHas C s

def MeasurableSpace.DynkinSystem.generate {α : Type u_3} (s : Set (Set α)) : MeasurableSpace.DynkinSystem α

The least Dynkin system containing a collection of basic sets.

Equations

• MeasurableSpace.DynkinSystem.generate s = { Has := MeasurableSpace.DynkinSystem.GenerateHas s, has_empty := ⋯, has_compl := ⋯, has_iUnion_nat := ⋯ }

theorem MeasurableSpace.DynkinSystem.generateHas_def {α : Type u_3} {C : Set (Set α)} : (MeasurableSpace.DynkinSystem.generate C).Has = MeasurableSpace.DynkinSystem.GenerateHas C

instance MeasurableSpace.DynkinSystem.instInhabited {α : Type u_3} : Inhabited (MeasurableSpace.DynkinSystem α)

Equations

• MeasurableSpace.DynkinSystem.instInhabited = { default := MeasurableSpace.DynkinSystem.generate Set.univ }

def MeasurableSpace.DynkinSystem.toMeasurableSpace {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) (h_inter : ∀ (s₁ s₂ : Set α), d.Has s₁ → d.Has s₂ → d.Has (s₁ ∩ s₂)) : MeasurableSpace α

If a Dynkin system is closed under binary intersection, then it forms a σ-algebra.

Equations

• d.toMeasurableSpace h_inter = { MeasurableSet' := d.Has, measurableSet_empty := ⋯, measurableSet_compl := ⋯, measurableSet_iUnion := ⋯ }

theorem MeasurableSpace.DynkinSystem.ofMeasurableSpace_toMeasurableSpace {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) (h_inter : ∀ (s₁ s₂ : Set α), d.Has s₁ → d.Has s₂ → d.Has (s₁ ∩ s₂)) : MeasurableSpace.DynkinSystem.ofMeasurableSpace (d.toMeasurableSpace h_inter) = d

def MeasurableSpace.DynkinSystem.restrictOn {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {s : Set α} (h : d.Has s) : MeasurableSpace.DynkinSystem α

If s is in a Dynkin system d, we can form the new Dynkin system {s ∩ t | t ∈ d}.

Equations

• d.restrictOn h = { Has := fun (t : Set α) => d.Has (t ∩ s), has_empty := ⋯, has_compl := ⋯, has_iUnion_nat := ⋯ }

theorem MeasurableSpace.DynkinSystem.generate_le {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {s : Set (Set α)} (h : ∀ t ∈ s, d.Has t) : MeasurableSpace.DynkinSystem.generate s ≤ d

theorem MeasurableSpace.DynkinSystem.generate_has_subset_generate_measurable {α : Type u_3} {C : Set (Set α)} {s : Set α} (hs : (MeasurableSpace.DynkinSystem.generate C).Has s) : MeasurableSet s

theorem MeasurableSpace.DynkinSystem.generate_inter {α : Type u_3} {s : Set (Set α)} (hs : IsPiSystem s) {t₁ : Set α} {t₂ : Set α} (ht₁ : (MeasurableSpace.DynkinSystem.generate s).Has t₁) (ht₂ : (MeasurableSpace.DynkinSystem.generate s).Has t₂) : (MeasurableSpace.DynkinSystem.generate s).Has (t₁ ∩ t₂)

theorem MeasurableSpace.DynkinSystem.generateFrom_eq {α : Type u_3} {s : Set (Set α)} (hs : IsPiSystem s) : MeasurableSpace.generateFrom s = (MeasurableSpace.DynkinSystem.generate s).toMeasurableSpace ⋯

Dynkin's π-λ theorem: Given a collection of sets closed under binary intersections, then the Dynkin system it generates is equal to the σ-algebra it generates. This result is known as the π-λ theorem. A collection of sets closed under binary intersection is called a π-system (often requiring additionally that it is non-empty, but we drop this condition in the formalization).

theorem MeasurableSpace.induction_on_inter {α : Type u_3} {C : Set α → Prop} {s : Set (Set α)} [m : MeasurableSpace α] (h_eq : m = MeasurableSpace.generateFrom s) (h_inter : IsPiSystem s) (h_empty : C ∅) (h_basic : ∀ t ∈ s, C t) (h_compl : ∀ (t : Set α), MeasurableSet t → C t → C tᶜ) (h_union : ∀ (f : ℕ → Set α), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)) ⦃t : Set α⦄ : MeasurableSet t → C t