isIntTangent

Mathlib.Geometry.Euclidean.Sphere.Tangent

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

English

Symmetry of IsIntTangentAt: if s1.IsIntTangentAt s2 p, then s2.IsIntTangentAt s1 p.

Русский

Симметрия IsIntTangentAt: если s1 внутренне касается s2 в p, то s2 касается s1 в p.

LaTeX

$$$ s_1.IsIntTangentAt s_2 p \\Rightarrow s_2.IsIntTangentAt s_1 p $$$

Lean4

theorem isIntTangent {s₁ s₂ : Sphere P} {p : P} (h : s₁.IsIntTangentAt s₂ p) : s₁.IsIntTangent s₂ :=
  ⟨p, h⟩

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

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

Разделы

Аффилиация

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