ball_eq_emptyset — Mathlib

English

If the radius is nonpositive, the ball is empty: p.ball x r = ∅ whenever r ≤ 0.

Русский

Если радиус неположителен, шар пуст: p.ball x r = ∅ при r ≤ 0.

LaTeX

$$$r \le 0 \Rightarrow p.ball x r = \emptyset$$$

Lean4

@[simp]
theorem ball_eq_emptyset (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : r ≤ 0) : p.ball x r = ∅ :=
  by
  ext
  rw [Seminorm.mem_ball, Set.mem_empty_iff_false, iff_false, not_lt]
  exact hr.trans (apply_nonneg p _)

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