theorem pi_lambda_theorem {α : Type u_1} {S : Set (Set α)} (hpi : IsPiSystem S) (d : MeasurableSpace.DynkinSystem α) (hS : ∀ s ∈ S, d.Has s) {s : Set α} (hs : MeasurableSet s) : d.Has s

π-λ theorem (Lecture 2, Dynkin's π-λ theorem): if P is a π-system and L is a λ-system (Dynkin system) containing P, then σ(P) ⊆ L. Concretely, if s is measurable with respect to the σ-algebra generated by a π-system S, and the Dynkin system d contains every set in S, then d also contains s.