nndist_left_midpoint — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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