dist_right_midpoint — Mathlib

English

The distance from p2 to the midpoint equals (2)^{-1} times the distance between p1 and p2.

Русский

Расстояние от p2 до середины равно расстоянию между p1 и p2, деленному на 2.

LaTeX

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

Lean4

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

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