isDiameter_iff_left_mem_and_midpoint_eq_center

English

A diameter equivalently satisfies that p1 belongs to the sphere and the midpoint of p1 and p2 is the center.

Русский

Диаметр эквивалентно тому, что p1 принадлежит сфере и середина p1 и p2 равна центру сферы.

LaTeX

$$$s.IsDiameter(p_1,p_2) \iff (p_1 \in s \land midpoint_{\\mathbb{R}}(p_1,p_2) = s.center)$$$

Lean4

theorem isDiameter_iff_left_mem_and_midpoint_eq_center : s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ midpoint ℝ p₁ p₂ = s.center :=
  ⟨fun h ↦ ⟨h.1, h.2⟩, fun h ↦ ⟨h.1, h.2⟩⟩

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