injective — Mathlib

English

There is a dilation α →ᵈ β corresponding to a function f: α → β, given a witness h that ∃ r ≠ 0 with ∀x,y, nndist(f x) (f y) = r · nndist x y.

Русский

Существует дилатация α →ᵈ β, соответствующая функции f: α → β, если есть доказательство существования r ≠ 0 такого, что ∀x,y, nndist(f x) (f y) = r · nndist x y.

LaTeX

$$∃ f, ∃ h, (∃ r ≠ 0, ∀ x y, nndist (f x) (f y) = r · nndist x y) ⇒ Dilation α β$$

Lean4

/-- A dilation from an emetric space is injective -/
protected theorem injective {α : Type*} [EMetricSpace α] [FunLike F α β] [DilationClass F α β] (f : F) : Injective f :=
  (antilipschitz f).injective

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