theorem absolutelyContinuous_def {Ω : Type u_1} {𝓕 : MeasurableSpace Ω} (μ ν : MeasureTheory.Measure Ω) : ν.AbsolutelyContinuous μ ↔ ∀ (A : Set Ω), μ A = 0 → ν A = 0

Definition (Absolutely continuous). For σ-finite measures μ and ν on (Ω, 𝓕), ν is absolutely continuous with respect to μ, written ν ≪ μ, if and only if every μ-null set A ⊆ Ω (i.e. μ A = 0) is also ν-null (i.e. ν A = 0). This lemma unfolds the Mathlib definition into this explicit characterization.