closedBall_zero' — Mathlib

English

The closed ball of radius 0 around x equals the closure of the singleton {x}.

Русский

Замкнутый шар радиуса 0 вокруг точки x равен замыканию множества {x}.

LaTeX

$$$\mathrm{closedBall}(x,0) = \overline{\{x\}}$$$

Lean4

theorem closedBall_zero' (x : α) : closedBall x 0 = closure { x } :=
  Subset.antisymm (fun _y hy => mem_closure_iff.2 fun _ε ε0 => ⟨x, mem_singleton x, (mem_closedBall.1 hy).trans_lt ε0⟩)
    (closure_minimal (singleton_subset_iff.2 (dist_self x).le) isClosed_closedBall)

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