isDiameter_iff_mem_and_mem_and_wbtw

English

Equivalently, a pair of points on a sphere forms a diameter iff the midpoint and perpendicular relations correspond to a diameter configuration.

Русский

Эквивалентно: две точки на сфере образуют диаметр тогда, когда середина отрезка и перпендикулярные отношения соответствуют конфигурации диаметра.

LaTeX

$$IsDiameter(s,p1,p2) \iff p1\in s \land p2\in s \land dist(p1,p2)=2\,s.radius$$

Lean4

theorem isDiameter_iff_mem_and_mem_and_wbtw : s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂ :=
  by
  refine ⟨fun h ↦ ⟨h.left_mem, h.right_mem, h.wbtw⟩, fun ⟨h₁, h₂, hr⟩ ↦ ?_⟩
  have hd := hr.dist_add_dist
  rw [mem_sphere.1 h₁, mem_sphere'.1 h₂, ← two_mul, eq_comm] at hd
  exact isDiameter_iff_mem_and_mem_and_dist.2 ⟨h₁, h₂, hd⟩

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