biUnion_lt_succ'

Mathlib.Data.Nat.Lattice

URI: https://scilib.ai/kg/mathlib#Set.biUnion_lt_succ'

English

For u: ℕ → Set α and n ∈ ℕ, the union over k < n+1 equals u0 union the union over k < n of u(k+1).

Русский

Для u: ℕ → Set α и n ∈ ℕ верно: ⋃_{k < n+1} u_k = u_0 ∪ ⋃_{k < n} u_{k+1}.

LaTeX

$$$\\displaystyle \\bigcup_{k < n+1} u_k = u_0 \\cup \\bigcup_{k < n} u_{k+1}.$$$

Lean4

theorem biUnion_lt_succ' (u : ℕ → Set α) (n : ℕ) : ⋃ k < n + 1, u k = u 0 ∪ ⋃ k < n, u (k + 1) :=
  Nat.iSup_lt_succ' u n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru