nndist_right_midpoint — Mathlib

English

The NN-distance from p2 to the midpoint equals (2)^{-1}_plus times the NN-distance between p1 and p2.

Русский

NN-расстояние от p2 до середины равно (2)^{-1}_плюс умноженному на NN-расстояние между p1 и p2.

LaTeX

$$$\mathrm{nndist}(p_2, \mathrm{midpoint}\; p_1\; p_2) = ‖2‖_+^{-1} \cdot \mathrm{nndist}(p_1,p_2)$$$

Lean4

@[simp]
theorem nndist_right_midpoint (p₁ p₂ : P) : nndist p₂ (midpoint 𝕜 p₁ p₂) = ‖(2 : 𝕜)‖₊⁻¹ * nndist p₁ p₂ :=
  NNReal.eq <| dist_right_midpoint _ _

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