English
Given f: α → β and a witness h that there exists r ≠ 0 with ∀x,y, nndist(f x) (f y) = r · nndist x y, one obtains a dilation α → β extending f with the same edist relation.
Русский
Пусть дано отображение f: α → β и свидетельство существования r ≠ 0 такое, что ∀x,y nndist(f x) (f y) = r · nndist x y; тогда получается дилатация, расширяющая f с тем же отношением расстояний.
LaTeX
$$∃ dilation α β, toFun := f, edist_eq' := ∃ r ≠ 0 ∧ ∀ x y, nndist (f x) (f y) = r · nndist x y$$
Lean4
/-- Alternative `Dilation` constructor when the distance hypothesis is over `nndist` -/
def mkOfNNDistEq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β)
(h : ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : α, nndist (f x) (f y) = r * nndist x y) : α →ᵈ β
where
toFun := f
edist_eq' := by
rcases h with ⟨r, hne, h⟩
refine ⟨r, hne, fun x y => ?_⟩
rw [edist_nndist, edist_nndist, ← ENNReal.coe_mul, h x y]
