iUnion_Icc_zsmul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iUnion_Icc_zsmul : ⋃ n : ℤ, Icc (n • p) ((n + 1) • p) = univ := by
  simpa only [zero_add] using iUnion_Icc_add_zsmul hp 0

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