closedBall_mem_nhds

Mathlib.Topology.MetricSpace.Pseudo.Defs

URI: https://scilib.ai/kg/mathlib#Metric.closedBall_mem_nhds

English

For every x and every ε>0, the closed ball centered at x is a neighborhood of x.

Русский

Для каждой точки x и ε>0 замкнутый шар вокруг x является окрестностью x.

LaTeX

$$closedBall(x, ε) ∈ 𝓝(x)$$

Lean4

theorem closedBall_mem_nhds (x : α) {ε : ℝ} (ε0 : 0 < ε) : closedBall x ε ∈ 𝓝 x :=
  mem_of_superset (ball_mem_nhds x ε0) ball_subset_closedBall

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru