biUnion_lt_succ — Mathlib

English

For a family of sets u: ℕ → Set α and n ∈ ℕ, the union over k < n+1 equals the union over k < n plus the k = n piece: ⋃ k < n+1, u_k = (⋃ k < n, u_k) ∪ u_n.

Русский

Для семейства множеств u: ℕ → Set α и числа n ∈ ℕ верна равенство ⋃_{k < n+1} u_k = (⋃_{k < n} u_k) ∪ u_n.

LaTeX

$$$\\displaystyle \\bigcup_{k < n+1} u_k = \\big(\\bigcup_{k < n} u_k\\big) \\cup u_n.$$$

Lean4

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

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