dist_eq — Mathlib

English

For any dilation f and points x,y, dist(f x, f y) = ratio(f) · dist(x,y).

Русский

Для дилатации f и точек x,y расстояние после применения дилатации равно ratio(f) умножить на расстояние до применения: dist(f x, f y) = ratio(f) · dist(x,y).

LaTeX

$$dist(f x, f y) = ratio f \cdot dist x y$$

Lean4

@[simp]
theorem dist_eq {α β F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β]
    (f : F) (x y : α) : dist (f x) (f y) = ratio f * dist x y := by simp only [dist_nndist, nndist_eq, NNReal.coe_mul]

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