right_mem

Mathlib.Geometry.Euclidean.Sphere.Basic

URI: https://scilib.ai/kg/mathlib#EuclideanGeometry.Sphere.IsDiameter.right_mem

← MathLib Explorer

English

If p1 and p2 are endpoints of a diameter of a sphere s, then p2 lies on s.

Русский

Если p1 и p2 являются концами диаметра сферы s, то p2 принадлежит сфере s.

LaTeX

$$$s.IsDiameter(p_1,p_2) \\Rightarrow p_2 \\in s$$$

Lean4

theorem right_mem (h : s.IsDiameter p₁ p₂) : p₂ ∈ s := by
  rw [mem_sphere, ← mem_sphere.1 h.left_mem, ← h.midpoint_eq_center, dist_left_midpoint_eq_dist_right_midpoint]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru