dirac_ne_dirac_iff — Mathlib

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⟩

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