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