Theorems · Theorem · measure theory

MeasureTheory.dirac_ne_dirac_iff_exists_measurableSet

∀ {α : Type u_1} [inst : MeasurableSpace α] {x y : α},
  MeasureTheory.Measure.dirac x ≠ MeasureTheory.Measure.dirac y ↔ ∃ A, MeasurableSet A ∧ x ∈ A ∧ y ∉ A

Dirac delta measures at two points are different if and only if there is a measurable set containing one of the points but not the other.

Defined in

Mathlib.MeasureTheory.Measure.Dirac

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace