closedBall_mem_nhds

Mathlib.Topology.EMetricSpace.Defs

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

English

If ε > 0, then closedBall x ε is a neighborhood of x.

Русский

Если ε>0, то замкнутый шар вокруг x радиуса ε образует окрестность x.

LaTeX

$$$\\text{If } \\varepsilon>0, \\ \\mathrm{closedBall}(x,\\varepsilon) \\in \\mathcal{N}(x)$$$

Lean4

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

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

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

Разделы

Аффилиация

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