isExtTangentAt_comm

Mathlib.Geometry.Euclidean.Sphere.Tangent

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

← MathLib Explorer

English

IsExtTangent is symmetric for two spheres: s1.IsExtTangent s2 ↔ s2.IsExtTangent s1.

Русский

IsExtTangent симметрично относительно двух сфер: s1.IsExtTangent s2 ↔ s2.IsExtTangent s1.

LaTeX

$$$ s_1.IsExtTangent s_2 \\iff s_2.IsExtTangent s_1 $$$

Lean4

theorem isExtTangentAt_comm {s₁ s₂ : Sphere P} {p : P} : s₁.IsExtTangentAt s₂ p ↔ s₂.IsExtTangentAt s₁ p :=
  ⟨IsExtTangentAt.symm, IsExtTangentAt.symm⟩

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

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

Разделы

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

Аффилиация

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