closedBall_mem_nhds — Mathlib

English

Let E be a Euclidean space with a standard topology. For every x ∈ E and every radius r > 0, the closed ball centered at x with radius r is a neighborhood of x.

Русский

Пусть E — евклидово пространство с обычной топологией. Для любой точки x ∈ E и любого радиуса r > 0 замкнутый шар с центром в x и радиусом r является окрестностью точки x.

LaTeX

$$$ \forall x \in E, \forall r > 0: \ \overline{B}(x,r) \in \mathcal{N}(x) $$$

Lean4

theorem closedBall_mem_nhds {x : E} {r : ℝ} (hr : 0 < r) : closedBall x r ∈ 𝓝 x :=
  nhds_basis_closedBall.mem_of_mem hr

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