nonempty_closedBall — Mathlib

English

An equivalent form is that closedBall x ε is nonempty exactly when ε ≥ 0.

Русский

Эквивалентная формулировка: замкнутый шар непустой тогда, когда ε ≥ 0.

LaTeX

$$$\\overline{B}(x, \\varepsilon) \\neq \\emptyset \\iff 0 \\le \\varepsilon$$$

Lean4

@[simp]
theorem nonempty_closedBall : (closedBall x ε).Nonempty ↔ 0 ≤ ε :=
  ⟨fun ⟨_x, hx⟩ => dist_nonneg.trans hx, fun h => ⟨x, mem_closedBall_self h⟩⟩

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