iUnion_closedBall_nat — Mathlib

English

The union over all natural numbers n of closedBalls around x with radius n equals the whole space.

Русский

Объединение по всем натуральным n замкнутых шаров around x радиуса n покрывает всю область.

LaTeX

$$$ \bigcup_{n \in \mathbb{N}} \overline{B}(x, n) = \text{univ} $$$

Lean4

@[simp]
theorem iUnion_closedBall_nat (x : α) : ⋃ n : ℕ, closedBall x n = univ :=
  iUnion_eq_univ_iff.2 fun y => exists_nat_ge (dist y x)

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