English
For any a and p > 0, the union over all integers n of the half-open interval Ico(a + n p, a + (n + 1) p) equals the whole space.
Русский
Для любых a и p > 0 объединение по всем целым n полуоткрытых интервалов Ico(a + n p, a + (n + 1) p) даёт всю область.
LaTeX
$$$\bigcup_{n\in\mathbb{Z}} Ico\bigl(a + n p,\; a + (n + 1) p\bigr) = \mathrm{Set.univ}$$$
Lean4
theorem iUnion_Ico_add_zsmul : ⋃ n : ℤ, Ico (a + n • p) (a + (n + 1) • p) = univ :=
by
refine eq_univ_iff_forall.mpr fun b => mem_iUnion.mpr ?_
rcases sub_toIcoDiv_zsmul_mem_Ico hp a b with ⟨hl, hr⟩
refine ⟨toIcoDiv hp a b, ⟨le_sub_iff_add_le.mp hl, ?_⟩⟩
rw [add_smul, one_smul, ← add_assoc]
convert sub_lt_iff_lt_add.mp hr using 1; abel