injective_dirac — Mathlib

English

The map x ↦ dirac x is injective when the space separates points.

Русский

Отображение x ↦ δ_x инъективно, если пространство разделяет точки.

LaTeX

$$$x \\neq y \\Rightarrow \\mathrm{dirac}_x \\neq \\mathrm{dirac}_y$$$

Lean4

/-- The assignment `x ↦ dirac x` is injective, assuming the measurable space separates points. -/
theorem injective_dirac [SeparatesPoints α] : Function.Injective (fun (x : α) ↦ dirac x) := fun x y x_ne_y ↦ by
  rwa [← dirac_eq_dirac_iff]

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