nndist_homothety_self — Mathlib

English

For p1, p2 in P and c in 𝕜, the nonnegative distance from the homothety image to p2 equals |1 − c|_+ times the nonnegative distance between p1 and p2.

Русский

Пусть p1, p2 ∈ P и c ∈ 𝕜. НН-расстояние между образом под гомотетией и p2 равно |1 − c|_+ умножить на НН-расстояние между p1 и p2.

LaTeX

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

Lean4

@[simp]
theorem nndist_homothety_self (p₁ p₂ : P) (c : 𝕜) : nndist (homothety p₁ c p₂) p₂ = ‖1 - c‖₊ * nndist p₁ p₂ :=
  NNReal.eq <| dist_homothety_self _ _ _

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