ball_eq_empty

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

Ball equals empty set iff ε ≤ 0.

Русский

Шар равен пустому множеству тогда и только тогда, когда ε ≤ 0.

LaTeX

$$$ ball x \varepsilon = \emptyset \iff \varepsilon \le 0 $$$

Lean4

@[simp]
theorem ball_eq_empty : ball x ε = ∅ ↔ ε ≤ 0 := by rw [← not_nonempty_iff_eq_empty, nonempty_ball, not_lt]

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

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

Разделы

Аффилиация

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