English
The set commonExtTangents(s1,s2) consists of those maximal common tangent spaces to s1 and s2 such that every point p in the tangent space does not lie weakly between the centers of s1 and s2 (Sbtw).
Русский
Общие внешние касательные — это такие касательные пространства, где никакая точка касания не лежит между центрами сфер.
LaTeX
$$$ as \\in s_1.commonExtTangents s_2 \\iff as \\in s_1.commonTangents s_2 \\land \\forall p \\in as, \\neg Sbtw \\ s_1.center \\ p \\ s_2.center $$$
Lean4
/-- The set of all maximal common external tangent spaces to the spheres `s₁` and `s₂`: tangent
spaces not containing a point strictly between the centers of the spheres. (In the degenerate case
where the two spheres are the same sphere with radius 0, the space is considered both an internal
and an external common tangent.) -/
def commonExtTangents (s₁ s₂ : Sphere P) : Set (AffineSubspace ℝ P) :=
{as ∈ s₁.commonTangents s₂ | ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center}
