English
If there exists r ≠ 0 with ∀x,y, dist(f x) (f y) = r · dist x y, then there is a dilation α → β with that edist relation.
Русский
Если существует r ≠ 0 такое, что ∀x,y dist(f x) (f y) = r · dist x y, то существует дилатация α → β с этим отношением расстояний.
LaTeX
$$∃ r ≠ 0, ∀ x y, dist(f x) (f y) = r · dist x y ⇒ Dilation α β$$
Lean4
/-- Alternative `Dilation` constructor when the distance hypothesis is over `dist` -/
def mkOfDistEq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β)
(h : ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : α, dist (f x) (f y) = r * dist x y) : α →ᵈ β :=
mkOfNNDistEq f <|
h.imp fun r hr => ⟨hr.1, fun x y => NNReal.eq <| by rw [coe_nndist, hr.2, NNReal.coe_mul, coe_nndist]⟩
