ball_bot — Mathlib

English

The ball around any point with a positive radius is nonempty; more specifically, ball (⊥) x r equals the whole space for r > 0.

Русский

Шар вокруг любой точки радиуса, все же положительного, непуст; например, ball(⊥) x r = всё пространство, если r > 0.

LaTeX

$$$0 < r \Rightarrow ball(\perp : Seminorm 𝕜 E) x r = \mathsf{Set.univ}$$$

Lean4

@[simp]
theorem ball_bot {r : ℝ} (x : E) (hr : 0 < r) : ball (⊥ : Seminorm 𝕜 E) x r = Set.univ :=
  ball_zero' x hr

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