commonIntTangents_union_commonExtTangents

English

The union of common internal tangents and common external tangents equals the set of all common tangents: commonIntTangents(s1,s2) ∪ commonExtTangents(s1,s2) = commonTangents(s1,s2).

Русский

Объединение общих внутренних и внешних касательных даёт все общие касательные: commonIntTangents(s1,s2) ∪ commonExtTangents(s1,s2) = commonTangents(s1,s2).

LaTeX

$$$ s_1.commonIntTangents s_2 \\cup s_1.commonExtTangents s_2 = s_1.commonTangents s_2 $$$

Lean4

@[simp]
theorem commonIntTangents_union_commonExtTangents (s₁ s₂ : Sphere P) :
    s₁.commonIntTangents s₂ ∪ s₁.commonExtTangents s₂ = s₁.commonTangents s₂ :=
  by
  ext as
  rw [Set.mem_union, mem_commonIntTangents_iff, mem_commonExtTangents_iff, ← and_or_left, and_iff_left_iff_imp]
  rintro -
  by_cases h : ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center
  · exact .inl h
  · refine .inr ?_
    simp_rw [not_exists, not_and] at h
    rintro p hp
    exact mt Sbtw.wbtw (h p hp)

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