ofDiameter — Mathlib

English

Construct the sphere with the given diameter p1 p2: its center is midpoint(p1,p2) and radius dist(p1,p2)/2.

Русский

Построим сферу по диаметру p1 p2: центр — середина p1 и p2, радиус — dist(p1,p2)/2.

LaTeX

$$Sphere.ofDiameter(p_1,p_2) = Sphere(center := midpoint(p_1,p_2), radius := dist(p_1,p_2)/2)$$

Lean4

/-- Construct the sphere with the given diameter. -/
protected def ofDiameter (p₁ p₂ : P) : Sphere P :=
  ⟨midpoint ℝ p₁ p₂, (dist p₁ p₂) / 2⟩

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