English
Dynkin's π-λ theorem: If s is a Pi-system, then generateFrom s equals the sigma-algebra generated by s; more precisely, generateFrom s = (generate s).toMeasurableSpace (generate_inter hs).
Русский
Теорема π-λ: если s — π-система, то σ-последовательность, порожденная s, совпадает с σ-алгеброй, порожденной s; точнее, generateFrom s = (generate s).toMeasurableSpace (generate_inter hs).
LaTeX
$$$ \text{IsPiSystem } s \; \Rightarrow\; generateFrom(s) = (generate(s)).toMeasurableSpace( generate\_inter( hs ) ). $$$
Lean4
/-- **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 generateFrom_eq {s : Set (Set α)} (hs : IsPiSystem s) :
generateFrom s = (generate s).toMeasurableSpace fun _ _ => generate_inter hs :=
le_antisymm (generateFrom_le fun t ht => GenerateHas.basic t ht)
(ofMeasurableSpace_le_ofMeasurableSpace_iff.mp <|
by
rw [ofMeasurableSpace_toMeasurableSpace]
exact generate_le _ fun t ht => measurableSet_generateFrom ht)
