dist_left_midpoint — Mathlib

English

The distance from p1 to the midpoint of p1 and p2 equals (1/2) times the distance between p1 and p2, i.e., dist(p1, midpoint(p1,p2)) = (2)^{-1} · dist(p1,p2).

Русский

Расстояние от p1 до середины отрезка p1p2 равно половине расстояния между p1 и p2.

LaTeX

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

Lean4

@[simp]
theorem dist_left_midpoint (p₁ p₂ : P) : dist p₁ (midpoint 𝕜 p₁ p₂) = ‖(2 : 𝕜)‖⁻¹ * dist p₁ p₂ := by
  rw [midpoint, dist_comm, dist_lineMap_left, invOf_eq_inv, ← norm_inv]

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