iUnion_Ioc_zsmul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iUnion_Ioc_zsmul : ⋃ n : ℤ, Ioc (n • p) ((n + 1) • p) = univ := by
  simpa only [zero_add] using iUnion_Ioc_add_zsmul hp 0

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