isOpen_ball

Mathlib.Topology.EMetricSpace.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem isOpen_ball : IsOpen (ball x ε) :=
  isOpen_iff.2 fun _ => exists_ball_subset_ball

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

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

Разделы

Аффилиация

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