English
The distance between the midpoints of (p1,p2) and (p3,p4) is at most (dist(p1,p3) + dist(p2,p4)) divided by the norm of 2, i.e., dist(midpoint(p1,p2), midpoint(p3,p4)) ≤ (dist(p1,p3) + dist(p2,p4)) / ||2||.
Русский
Расстояние между серединами (p1,p2) и (p3,p4) не превосходит (dist(p1,p3) + dist(p2,p4)) / ||2||.
LaTeX
$$$\mathrm{dist}(\mathrm{midpoint}\; p_1\; p_2,\; \mathrm{midpoint}\; p_3\; p_4) \leq \frac{\mathrm{dist}(p_1,p_3) + \mathrm{dist}(p_2,p_4)}{\|2\|}$$$
Lean4
theorem dist_midpoint_midpoint_le' (p₁ p₂ p₃ p₄ : P) :
dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖(2 : 𝕜)‖ :=
by
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, midpoint_vsub_midpoint]
rw [midpoint_eq_smul_add, norm_smul, invOf_eq_inv, norm_inv, ← div_eq_inv_mul]
grw [norm_add_le]
