dist_homothety_self — Mathlib

English

For any p1, p2 in P and any c in 𝕜, the distance from the image of p2 under the homothety with center p1 and coefficient c to p2 equals |1 − c| times the distance between p1 and p2.

Русский

Пусть p1, p2 ∈ P и c ∈ 𝕜. Расстояние между p2 и точкой, полученной гомотетией с центром p1 и коэффициентом c, равно |1 − c| умножить на расстояние между p1 и p2.

LaTeX

$$$\mathrm{dist}(\mathrm{homothety}(p_1,c,p_2),\; p_2) = ‖1 - c‖ \cdot \mathrm{dist}(p_1,p_2)$$$

Lean4

@[simp]
theorem dist_homothety_self (p₁ p₂ : P) (c : 𝕜) : dist (homothety p₁ c p₂) p₂ = ‖1 - c‖ * dist p₁ p₂ := by
  rw [homothety_eq_lineMap, dist_lineMap_right]

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