iUnion_Icc_add_zsmul — Mathlib

English

For any a and p > 0, the union over all integers n of the closed interval Icc(a + n p, a + (n + 1) p) equals the whole space.

Русский

Для любых a и p > 0 объединение по всем целым n замкнутых интервалов Icc(a + n p, a + (n + 1) p) даёт всю область.

LaTeX

$$$\bigcup_{n\in\mathbb{Z}} Icc\bigl(a + n p,\; a + (n + 1) p\bigr) = \mathrm{Set.univ}$$$

Lean4

theorem iUnion_Icc_add_zsmul : ⋃ n : ℤ, Icc (a + n • p) (a + (n + 1) • p) = univ := by
  simpa only [iUnion_Ioc_add_zsmul hp a, univ_subset_iff] using
    iUnion_mono fun n : ℤ => (Ioc_subset_Icc_self : Ioc (a + n • p) (a + (n + 1) • p) ⊆ Icc _ _)

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