iUnion_Ioc_intCast — Mathlib

English

For any α with a ring structure, the union over n ∈ ℤ of Ioc(n.cast, n.cast + 1) equals the whole space.

Русский

Для кольца α объединение по целым n интервалов Ioc(n.cast, n.cast + 1) даёт всю область.

LaTeX

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

Lean4

theorem iUnion_Ioc_intCast : ⋃ n : ℤ, Ioc (n : α) (n + 1) = Set.univ := by
  simpa only [zero_add] using iUnion_Ioc_add_intCast (0 : α)

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