Theorems · Theorem · measure theory

MeasureTheory.measureReal_eq_measureReal_iff

∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  {m : MeasurableSpace β} {ν : MeasureTheory.Measure β} {t : Set β},
  autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_eq_measureReal_iff._auto_1 →
    autoParam (ν t ≠ ⊤) MeasureTheory.measureReal_eq_measureReal_iff._auto_3 → (μ.real s = ν.real t ↔ μ s = ν t)

Defined in

Mathlib.MeasureTheory.Measure.Real

Cited by

5 results in Mathlib

Foundations

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