iUnion_Ioc_add_intCast — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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