mem_of_mem_tangentsFrom

Mathlib.Geometry.Euclidean.Sphere.Tangent

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

English

If as ∈ tangentsFrom p, then p ∈ as.

Русский

Если $as \\in \\mathrm{tangentsFrom}(s,p)$, то $p \\in as$.

LaTeX

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

Lean4

theorem mem_of_mem_tangentsFrom {as : AffineSubspace ℝ P} {s : Sphere P} {p : P} (h : as ∈ s.tangentsFrom p) : p ∈ as :=
  h.2

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

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

Разделы

Аффилиация

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