eball_top_eq_univ — Mathlib

English

The open ball of infinite radius is the whole space: for any x, EMetric.ball x ∞ equals the entire space.

Русский

Открытый шар бесконечного радиуса совпадает с всей пространством: EMetric.ball x ∞ = всё пространство.

LaTeX

$$$\\forall x,\\ EMetric.ball(x, \\infty) = \\mathrm{univ}$.$$

Lean4

/-- In a pseudometric space, an open ball of infinite radius is the whole space -/
theorem eball_top_eq_univ (x : α) : EMetric.ball x ∞ = Set.univ :=
  Set.eq_univ_iff_forall.mpr fun y => edist_lt_top y x

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