ball_eq_empty_iff — Mathlib

English

The ball is empty precisely when the radius is zero.

Русский

Шар пуст ровно тогда, когда радиус равен нулю.

LaTeX

$$$\\mathrm{ball}(x,\\varepsilon) = \\emptyset \\iff \\varepsilon = 0$$$

Lean4

theorem ball_eq_empty_iff : ball x ε = ∅ ↔ ε = 0 :=
  eq_empty_iff_forall_notMem.trans
    ⟨fun h => le_bot_iff.1 (le_of_not_gt fun ε0 => h _ (mem_ball_self ε0)), fun ε0 _ h =>
      not_lt_of_ge (le_of_eq ε0) (pos_of_mem_ball h)⟩

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