dist_self_homothety — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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