isOpen_ball

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

For any x and any radius ε, the metric open ball B(x, ε) is open.

Русский

Для любых x и ε шар B(x, ε) открыт.

LaTeX

$$$IsOpen(B(x, \varepsilon))$$$

Lean4

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

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

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

Разделы

Аффилиация

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