Theorems · Theorem · measure theory

MeasureTheory.ae_eq_of_subset_of_measure_ge

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  s ⊆ t → μ t ≤ μ s → MeasureTheory.NullMeasurableSet s μ → μ t ≠ ⊤ → s =ᵐ[μ] t

If s ⊆ t, μ t ≤ μ s, μ t ≠ ∞, and s is measurable, then s =ᵐ[μ] t.

Defined in

Mathlib.MeasureTheory.Measure.MeasureSpace

Cited by

3 results in Mathlib

Foundations

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