dist_midpoint_left — Mathlib

English

The distance from the midpoint to p1 equals the same as from p1 to midpoint, i.e., dist(midpoint, p1) = (2)^{-1} · dist(p1, p2).

Русский

Расстояние от середины до p1 равно расстоянию от p1 до середины: dist(midpoint, p1) = 2^{-1} dist(p1,p2).

LaTeX

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

Lean4

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

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