isDiameter_iff_mem_and_mem_and_dist

English

For a sphere s and points p1, p2, s.IsDiameter p1 p2 holds iff p1 and p2 lie on s and the distance dist(p1,p2) equals 2 times the radius.

Русский

Для сферы s и точек p1, p2 верно: s.IsDiameter p1 p2 тогда и только тогда, когда p1,p2 лежат на s и расстояние dist(p1,p2) равно 2 радиусу.

LaTeX

$$$s.IsDiameter(p_1,p_2) \iff p_1\in s \land p_2\in s \land dist(p_1,p_2)=2\cdot s.radius$$$

Lean4

theorem isDiameter_iff_mem_and_mem_and_dist : s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius :=
  by
  refine ⟨fun h ↦ ⟨h.left_mem, h.right_mem, h.dist_left_right⟩, fun ⟨h₁, h₂, hr⟩ ↦ ⟨h₁, ?_⟩⟩
  rw [midpoint_eq_iff, AffineEquiv.pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq]
  apply eq_of_norm_eq_of_norm_add_eq
  · simp_rw [← dist_eq_norm_vsub, mem_sphere'.1 h₁, mem_sphere.1 h₂]
  · simp_rw [vsub_add_vsub_cancel, ← dist_eq_norm_vsub, mem_sphere'.1 h₁, mem_sphere.1 h₂]
    rw [dist_comm, hr, two_mul]

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