nndist_midpoint_midpoint_le' — Mathlib

English

The NN-distance between the midpoints of (p1,p2) and (p3,p4) is at most (nndist(p1,p3) + nndist(p2,p4)) divided by the NN-norm of 2.

Русский

NN-расстояние между серединами равно не более чем (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₄ : P) :
    nndist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (nndist p₁ p₃ + nndist p₂ p₄) / ‖(2 : 𝕜)‖₊ :=
  dist_midpoint_midpoint_le' _ _ _ _

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