self_mem_orthRadius

Mathlib.Geometry.Euclidean.Sphere.Tangent

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

English

For any sphere s and any point p, p belongs to s.orthRadius(p).

Русский

Для сферы s и точки p, p принадлежит s.orthRadius(p).

LaTeX

$$$p \\in s.orthRadius(p)$$$

Lean4

theorem self_mem_orthRadius (s : Sphere P) (p : P) : p ∈ s.orthRadius p :=
  self_mem_mk' _ _

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

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

Разделы

Аффилиация

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