ball_mem_nhds

Mathlib.Topology.EMetricSpace.Defs

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

English

IsOpen (ball x ε) holds for all x and ε.

Русский

Открытый шар вокруг x радиуса ε является открытым.

LaTeX

$$$\\text{IsOpen}(\\mathrm{ball}(x,\\varepsilon))$$$

Lean4

theorem ball_mem_nhds (x : α) {ε : ℝ≥0∞} (ε0 : 0 < ε) : ball x ε ∈ 𝓝 x :=
  isOpen_ball.mem_nhds (mem_ball_self ε0)

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

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

Разделы

Аффилиация

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