ball_mem_nhds

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

For every x and every ε>0, B(x, ε) belongs to the neighborhood filter at x.

Русский

Для любой точки x и любого ε>0 шар B(x, ε) принадлежит к окрестностям x.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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