isIntTangentAt_self_iff_mem

Mathlib.Geometry.Euclidean.Sphere.Tangent

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

English

For any sphere s and point p, s.IsIntTangentAt s p iff p ∈ s.

Русский

Для сферы s и точки p верно: s.IsIntTangentAt s p ⇔ p ∈ s.

LaTeX

$$$ s.IsIntTangentAt s p \\iff p \\in s $$$

Lean4

@[simp]
theorem isIntTangentAt_self_iff_mem {s : Sphere P} {p : P} : s.IsIntTangentAt s p ↔ p ∈ s :=
  ⟨fun ⟨h, _, _⟩ ↦ h, fun h ↦ ⟨h, h, by simp⟩⟩

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

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

Разделы

Аффилиация

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