isIntTangentAt_center_iff — Mathlib

English

For spheres s1 and s2, s1.IsIntTangentAt s2 s1.center holds iff s1.radius = 0 and s1.center ∈ s2.

Русский

Для сфер s1 и s2, s1.IsIntTangentAt s2 s1.center выполняется тогда, когда радиус s1 равен 0 и центр s1 принадлежит s2.

LaTeX

$$$ s_1.IsIntTangentAt s_2 s_1.center \\iff s_1.radius = 0 \\land s_1.center \\in s_2 $$$

Lean4

theorem isIntTangentAt_center_iff {s₁ s₂ : Sphere P} :
    s₁.IsIntTangentAt s₂ s₁.center ↔ s₁.radius = 0 ∧ s₁.center ∈ s₂ :=
  by
  refine ⟨?_, ?_⟩
  · rintro ⟨h₁, h₂, -⟩
    rw [center_mem_iff] at h₁
    exact ⟨h₁, h₂⟩
  · rintro ⟨hr, hc⟩
    refine ⟨?_, hc, ?_⟩
    · rw [center_mem_iff, hr]
    · simp

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