injective_diracProba — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The assignment `x ↦ diracProba x` is injective if all singletons are measurable. -/
theorem injective_diracProba {X : Type*} [MeasurableSpace X] [MeasurableSpace.SeparatesPoints X] :
    Function.Injective (fun (x : X) ↦ diracProba x) :=
  by
  intro x y x_eq_y
  rw [← dirac_eq_dirac_iff]
  rwa [Subtype.ext_iff] at x_eq_y

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