dist_left_lineMap — Mathlib

English

The distance from p to the homothety of p toward q by factor c is |c| times the distance from p to q.

Русский

Расстояние до гомотетии точки p к точке q с коэффициентом c равно |c| умножить на расстояние p к q.

LaTeX

$$$$ \mathrm{dist}(p, \mathrm{homothety}(p,c,q)) = |c| \cdot \mathrm{dist}(p,q). $$$$

Lean4

@[simp]
theorem dist_left_lineMap (p₁ p₂ : P) (c : 𝕜) : dist p₁ (lineMap p₁ p₂ c) = ‖c‖ * dist p₁ p₂ :=
  (dist_comm _ _).trans (dist_lineMap_left _ _ _)

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