nndist_self_homothety — Mathlib

English

For p1, p2 in P and c in 𝕜, the NN-distance from the homothety image to p2 equals |1 − c|_+ times the NN-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_self_homothety (p₁ p₂ : P) (c : 𝕜) : nndist p₂ (homothety p₁ c p₂) = ‖1 - c‖₊ * nndist p₁ p₂ :=
  NNReal.eq <| dist_self_homothety _ _ _

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