iUnion_Ico_intCast — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iUnion_Ico_intCast : ⋃ n : ℤ, Ico (n : α) (n + 1) = Set.univ := by
  simpa only [zero_add] using iUnion_Ico_add_intCast (0 : α)

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