isIntTangent_self_iff — Mathlib

English

For a sphere s in a Euclidean space, s is internally tangent to itself if and only if the radius is nonnegative.

Русский

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

LaTeX

$$$s\text{ IsIntTangent } s \;\Leftrightarrow\; 0 \le s.\text{radius}$$$

Lean4

@[simp]
theorem isIntTangent_self_iff [Nontrivial V] {s : Sphere P} : s.IsIntTangent s ↔ 0 ≤ s.radius :=
  by
  simp_rw [IsIntTangent, isIntTangentAt_self_iff_mem]
  rw [← nonempty_iff]
  simp [Set.Nonempty]

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