English
The set commonIntTangents(s1,s2) consists of all maximal tangent spaces to both spheres s1 and s2 that contain a point p with p weakly between the centers of the spheres. Formally, as ∈ s1.commonIntTangents s2 iff as ∈ s1.commonTangents s2 and ∃ p ∈ as with Wbtw(center(s1), p, center(s2)).
Русский
Множество общих внутренних касательных состоит из тех же касательных, которые проходят между центрами сфер.
LaTeX
$$$ as \\in s_1.commonIntTangents s_2 \\iff as \\in s_1.commonTangents s_2 \\land \\exists p \\in as, Wbtw( s_1.center, p, s_2.center ) $$$
Lean4
/-- The set of all maximal common internal tangent spaces to the spheres `s₁` and `s₂`: tangent
spaces containing a point weakly between the centers of the spheres. -/
def commonIntTangents (s₁ s₂ : Sphere P) : Set (AffineSubspace ℝ P) :=
{as ∈ s₁.commonTangents s₂ | ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center}
