subsingleton_closedBall — Mathlib

English

If r ≤ 0, then closedBall(x,r) is a subsingleton (indeed empty if r<0, singleton if r=0).

Русский

Если r ≤ 0, то закрытый шар вокруг x является подсинглотоном (пуст, если r<0, синглтон — если r=0).

LaTeX

$$(r ≤ 0) → (closedBall\;x\;r) \text{ isSubsingleton}$$

Lean4

theorem subsingleton_closedBall (x : γ) {r : ℝ} (hr : r ≤ 0) : (closedBall x r).Subsingleton :=
  by
  rcases hr.lt_or_eq with (hr | rfl)
  · rw [closedBall_eq_empty.2 hr]
    exact subsingleton_empty
  · rw [closedBall_zero]
    exact subsingleton_singleton

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