isExtTangent

Mathlib.Geometry.Euclidean.Sphere.Tangent

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

English

Symmetry of IsExtTangentAt: if s1.IsExtTangentAt s2 p, then s2.IsExtTangentAt s1 p with swapped sides.

Русский

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

LaTeX

$$$ s_1.IsExtTangentAt s_2 p \\Rightarrow s_2.IsExtTangentAt s_1 p $$$

Lean4

theorem isExtTangent {s₁ s₂ : Sphere P} {p : P} (h : s₁.IsExtTangentAt s₂ p) : s₁.IsExtTangent s₂ :=
  ⟨p, h⟩

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

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

Разделы

Аффилиация

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