iUnion_ball_nat_succ — Mathlib

English

The union over all natural numbers n of the balls B(x, n+1) equals the entire space: ⋃_{n∈N} ball x (n+1) = univ.

Русский

Объединение по всем натуральным числам n шаров B(x, n+1) равно всей пространству.

LaTeX

$$$ \bigcup_{n \in \mathbb{N}} \mathrm{ball}(x, n+1) = \mathsf{univ} $$$

Lean4

@[simp]
theorem iUnion_ball_nat_succ (x : α) : ⋃ n : ℕ, ball x (n + 1) = univ :=
  iUnion_eq_univ_iff.2 fun y => (exists_nat_gt (dist y x)).imp fun _ h => h.trans (lt_add_one _)

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