iUnion_Icc_intCast — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iUnion_Icc_intCast : ⋃ n : ℤ, Icc (n : α) (n + 1) = Set.univ := by
  simpa only [zero_add] using iUnion_Icc_add_intCast (0 : α)

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