ofDiameter_eq — Mathlib

English

A sphere s has diameter p1 p2 iff s = Sphere.ofDiameter p1 p2.

Русский

Сфера s имеет диаметр p1 p2 тогда и только тогда, когда s равна Sphere.ofDiameter p1 p2.

LaTeX

$$s.IsDiameter(p_1,p_2) \iff Sphere.ofDiameter(p_1,p_2) = s$$

Lean4

theorem ofDiameter_eq (h : s.IsDiameter p₁ p₂) : .ofDiameter p₁ p₂ = s :=
  by
  ext
  · simp [Sphere.ofDiameter, h.midpoint_eq_center]
  · simp [Sphere.ofDiameter, ← h.dist_left_right_div_two]

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