iUnion_Ico_add_intCast — Mathlib

English

For any a, the union over all integers n of Ico (a + n.cast) (a + (n.cast) + 1) equals the whole space.

Русский

Для любого a объединение по всем целым n интервалов Ico(a + n.cast) (a + (n.cast) + 1) даёт всю область.

LaTeX

$$$\bigcup_{n\in\mathbb{Z}} Ico\bigl(a + n^{\text{cast}},\; a + (n^{\text{cast}}) + 1\bigr) = \mathrm{Set.univ}$$$

Lean4

theorem iUnion_Ico_add_intCast : ⋃ n : ℤ, Ico (a + n) (a + n + 1) = Set.univ := by
  simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using iUnion_Ico_add_zsmul zero_lt_one a

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