ball_subset_interior_closedBall — Mathlib

English

In any metric space, every open ball is contained in the interior of the corresponding closed ball.

Русский

В любом метрическом пространстве любая открытая шарa содержится внутри внутренности соответствующей замкнутой шары.

LaTeX

$$$\text{ball }(x,\varepsilon) \subseteq \operatorname{interior}(\operatorname{closedBall}(x,\varepsilon))$$$

Lean4

theorem ball_subset_interior_closedBall : ball x ε ⊆ interior (closedBall x ε) :=
  interior_maximal ball_subset_closedBall isOpen_ball

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