closure_closedBall — Mathlib

English

The closure of a closed ball is the closed ball itself; i.e., closed balls are closed sets.

Русский

Замыкание замкнутого шара равно самому шару; то есть замкнутые шары замкнуты.

LaTeX

$$$\mathrm{closure}(\mathrm{closedBall}(x,\varepsilon)) = \mathrm{closedBall}(x,\varepsilon)$$$

Lean4

@[simp]
theorem closure_closedBall : closure (closedBall x ε) = closedBall x ε :=
  isClosed_closedBall.closure_eq

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