commonTangents — Mathlib

English

The set of all maximal tangent spaces common to two spheres s1 and s2 is the intersection of their tangent sets: commonTangents(s1,s2) = tangentSet(s1) ∩ tangentSet(s2).

Русский

Множество всех максимальных общих касательных пространств двух сфер s1 и s2 равно пересечению их касательных множеств: commonTangents(s1,s2) = tangentSet(s1) ∩ tangentSet(s2).

LaTeX

$$$ \\mathrm{commonTangents}(s_1,s_2) = s_1.tangentSet \\cap s_2.tangentSet $$$

Lean4

/-- The set of all maximal common tangent spaces to the spheres `s₁` and `s₂`. -/
def commonTangents (s₁ s₂ : Sphere P) : Set (AffineSubspace ℝ P) :=
  s₁.tangentSet ∩ s₂.tangentSet

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