isTangentAt_center_iff — Mathlib

English

For a sphere S and affine subspace as, S is tangent at its center to as if and only if radius is zero and the center lies in as.

Русский

Для сферы S и аффинного подпространства as касание в центре сферы возможно тогда и только тогда, когда радиус равен нулю и центр принадлежит as.

LaTeX

$$$ s.IsTangentAt s.center as \\iff (s.radius = 0 \uplus s.center \\in as) $$$

Lean4

theorem isTangentAt_center_iff {s : Sphere P} {as : AffineSubspace ℝ P} :
    s.IsTangentAt s.center as ↔ s.radius = 0 ∧ s.center ∈ as :=
  by
  refine ⟨?_, ?_⟩
  · rintro ⟨hr, hm, -⟩
    rw [center_mem_iff] at hr
    exact ⟨hr, hm⟩
  · rintro ⟨hr, hm⟩
    refine ⟨?_, hm, ?_⟩
    · rw [center_mem_iff, hr]
    · simp

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