nndist_midpoint_midpoint_le — Mathlib

English

For p1, p2, p3, p4 in V, the NN-distance between the midpoints of (p1,p2) and (p3,p4) is at most (nndist(p1,p3) + nndist(p2,p4)) / 2.

Русский

NN-расстояние между серединами отрезков (p1,p2) и (p3,p4) не превосходит (nndist(p1,p3) + nndist(p2,p4)) / 2.

LaTeX

$$$\mathrm{nndist}(\mathrm{midpoint}\; p_1\; p_2,\; \mathrm{midpoint}\; p_3\; p_4) \leq \frac{\mathrm{nndist}(p_1,p_3) + \mathrm{nndist}(p_2,p_4)}{2}$$$

Lean4

theorem nndist_midpoint_midpoint_le (p₁ p₂ p₃ p₄ : V) :
    nndist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (nndist p₁ p₃ + nndist p₂ p₄) / 2 :=
  dist_midpoint_midpoint_le _ _ _ _

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