isDiameter_iff_right_mem_and_pointReflection_center_right

English

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

Русский

Если p1-п3 и p2-п3 являются диаметрами, то p1 = p2.

LaTeX

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

Lean4

theorem isDiameter_iff_right_mem_and_pointReflection_center_right :
    s.IsDiameter p₁ p₂ ↔ p₂ ∈ s ∧ Equiv.pointReflection s.center p₂ = p₁ := by
  rw [isDiameter_comm, isDiameter_iff_left_mem_and_pointReflection_center_left]

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