closedBall_eq_empty

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

A closed ball is empty if and only if its radius is negative.

Русский

Замкнутый шар пуст, если и только если радиус отрицателен.

LaTeX

$$closedBall x ε = ∅ \\iff ε < 0$$

Lean4

@[simp]
theorem closedBall_eq_empty : closedBall x ε = ∅ ↔ ε < 0 := by
  rw [← not_nonempty_iff_eq_empty, nonempty_closedBall, not_le]

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

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

Разделы

Аффилиация

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