injective — Mathlib

English

AntilipschitzWith K f implies f is injective.

Русский

Антилипшицево отображение с константой K влечёт инъективность f.

LaTeX

$$$\\text{Injective}(f)$$$

Lean4

protected theorem injective {α : Type*} {β : Type*} [EMetricSpace α] [PseudoEMetricSpace β] {K : ℝ≥0} {f : α → β}
    (hf : AntilipschitzWith K f) : Function.Injective f := fun x y h => by
  simpa only [h, edist_self, mul_zero, edist_le_zero] using hf x y

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