closedBall_top — Mathlib

English

The closed ball of infinite radius around any x is the entire space: closedBall(x, ∞) = universal set.

Русский

Закрытая окрестность с бесконечным радиусом вокруг любой точки — это вся пространство.

LaTeX

$$$ \operatorname{closedBall}(x, \infty) = \mathsf{univ}. $$$

Lean4

@[simp]
theorem closedBall_top (x : α) : closedBall x ∞ = univ :=
  eq_univ_of_forall fun _ => mem_setOf.2 le_top

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