orthRadius_eq_orthRadius_iff — Mathlib

English

For a sphere S and points p,q, the orthRadius at p equals the orthRadius at q if and only if p = q.

Русский

Для сферы S и точек p, q выполняется: s.orthRadius(p) = s.orthRadius(q) тогда и только тогда, когда p = q.

LaTeX

$$$ s.orthRadius(p) = s.orthRadius(q) \\iff p = q $$$

Lean4

@[simp]
theorem orthRadius_eq_orthRadius_iff {s : Sphere P} {p q : P} : s.orthRadius p = s.orthRadius q ↔ p = q :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩
  have hpq := orthRadius_le_orthRadius_iff.1 h.le
  have hqp := orthRadius_le_orthRadius_iff.1 h.symm.le
  grind

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