Theorems · Theorem · measure theory

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).

Defined in

Mathlib.MeasureTheory.PiSystem

Cited by

1 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound