mem_commonIntTangents_iff — Mathlib

English

For any spheres s1, s2 and point p, if s1 is externally tangent to s2 at p, then s2 is externally tangent to s1 at p.

Русский

Для любых сфер s1, s2 и точки p, если сфера s1 внешне касается s2 в p, то сфера s2 внешне касается s1 в p.

LaTeX

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

Lean4

theorem mem_commonIntTangents_iff {as : AffineSubspace ℝ P} {s₁ s₂ : Sphere P} :
    as ∈ s₁.commonIntTangents s₂ ↔ as ∈ s₁.commonTangents s₂ ∧ ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center :=
  Iff.rfl

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