iUnion_ball_nat — Mathlib

English

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

Русский

Объединение по всем натуральным числам n шаров B(x,n) равно всей пространству: ⋃_{n∈N} ball x n = univ.

LaTeX

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

Lean4

@[simp]
theorem iUnion_ball_nat (x : α) : ⋃ n : ℕ, ball x n = univ :=
  iUnion_eq_univ_iff.2 fun y => exists_nat_gt (dist y x)

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