IsIntTangent

Mathlib.Geometry.Euclidean.Sphere.Tangent

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

← MathLib Explorer

English

IsExtTangent is symmetric with respect to the two spheres.

Русский

IsExtTangent симметрично по отношению к двум сферам.

LaTeX

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

Lean4

/-- The sphere `s₁` is internally tangent to the sphere `s₂` at some point. -/
def IsIntTangent (s₁ s₂ : Sphere P) : Prop :=
  ∃ p, s₁.IsIntTangentAt s₂ p

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

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

Разделы

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

Аффилиация

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