theorem measurability_from_generators {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {S : Set (Set β)} {f : α → β} : Measurable f ↔ ∀ s ∈ S, MeasurableSet (f ⁻¹' s)

Measurability from generators (Lecture 3, "Defining random variables"): a map f : α → β is measurable for the σ-algebra generated by a family S of subsets of β if and only if f ⁻¹' s is measurable for every s ∈ S. Equivalently, to check measurability it suffices to check it on a generating family of the target σ-algebra.