isTangent_of_mem_tangentsFrom

Mathlib.Geometry.Euclidean.Sphere.Tangent

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

← MathLib Explorer

English

If as ∈ tangentsFrom p, then s.IsTangent as.

Русский

Если $as \\in \\mathrm{tangentsFrom}(s,p)$, то сфера $s$ касается $as$.

LaTeX

$$$ as \\in s.tangentsFrom(p) \\Rightarrow s.IsTangent as $$$

Lean4

theorem isTangent_of_mem_tangentsFrom {as : AffineSubspace ℝ P} {s : Sphere P} {p : P} (h : as ∈ s.tangentsFrom p) :
    s.IsTangent as :=
  isTangent_of_mem_tangentSet h.1

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

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

Разделы

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

Аффилиация

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