English
In a space that separates points, δ_x ≠ δ_y whenever x ≠ y.
Русский
В пространстве, разделяющем точки, δ_x ≠ δ_y при x ≠ y.
LaTeX
$$$x \\neq y \\Rightarrow \\mathrm{dirac}_x \\neq \\mathrm{dirac}_y$$$
Lean4
/-- Dirac delta measures at two points are different if and only if the two points are different,
assuming the measurable space separates points. -/
theorem dirac_ne_dirac_iff [SeparatesPoints α] {x y : α} : Measure.dirac x ≠ Measure.dirac y ↔ x ≠ y :=
⟨fun h x_eq_y ↦ h <| congrArg dirac x_eq_y, fun h ↦ dirac_ne_dirac h⟩