iUnion_Ico_add_zsmul — Mathlib

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

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