isDiameter_iff_left_mem_and_pointReflection_center_left

English

If p1-p2 and p1-p3 are diameters of s, then p2 = p3.

Русский

Если p1-p2 и p1-p3 являются диаметрами сферы s, то p2 = p3.

LaTeX

$$s.IsDiameter(p_1,p_2) \rightarrow s.IsDiameter(p_1,p_3) \rightarrow p_2 = p_3$$

Lean4

theorem isDiameter_iff_left_mem_and_pointReflection_center_left :
    s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ Equiv.pointReflection s.center p₁ = p₂ :=
  ⟨fun h ↦ ⟨h.1, h.pointReflection_center_left⟩, fun h ↦ ⟨h.1, by simp [← h.2]⟩⟩

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