closedBall_eq_emptyset — Mathlib

English

If the radius is negative, the closed ball centered at any point is empty: for any x and p, p.closedBall x r = ∅ whenever r < 0.

Русский

Если радиус отрицателен, замкнутый шар с центром в x пуст: для любого x и p, p.closedBall x r = ∅ тогда, когда r < 0.

LaTeX

$$$\forall x\in E,\forall r\in\mathbb{R},\; r<0\;\Rightarrow\; p.closedBall x r = \emptyset$$$

Lean4

@[simp]
theorem closedBall_eq_emptyset (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : r < 0) : p.closedBall x r = ∅ :=
  by
  ext
  rw [Seminorm.mem_closedBall, Set.mem_empty_iff_false, iff_false, not_le]
  exact hr.trans_le (apply_nonneg _ _)

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