dirac_ne_dirac — Mathlib

English

There is a measurable set distinguishing x and y if and only if δ_x ≠ δ_y.

Русский

Существует измеримое множество, отделяющее x и y, если и только если δ_x ≠ δ_y.

LaTeX

$$$\\mathrm{dirac}_x \\neq \\mathrm{dirac}_y \\iff \\exists A, \\text{MeasurableSet}(A) \\land x\\in A \\land y\\notin A$$$

Lean4

/-- Dirac delta measures at two different points are different, assuming the measurable space
separates points. -/
theorem dirac_ne_dirac [SeparatesPoints α] {x y : α} (x_ne_y : x ≠ y) : Measure.dirac x ≠ Measure.dirac y :=
  by
  obtain ⟨A, A_mble, x_in_A, y_notin_A⟩ := exists_measurableSet_of_ne x_ne_y
  exact dirac_ne_dirac_iff_exists_measurableSet.mpr ⟨A, A_mble, x_in_A, y_notin_A⟩

Похожие утверждения