union_iUnion_nat_succ — Mathlib

English

For a family u: ℕ → Set α, the union of u(0) with the union over i of u(i+1) equals the union over i of u(i).

Русский

Для семейства u: ℕ → Set α объединение u(0) и объединение по i у которых i+1 заменяет все i, равно объединению по i.

LaTeX

$$$u(0) \\cup \\bigcup_i u(i+1) = \\bigcup_i u(i)$$$

Lean4

theorem union_iUnion_nat_succ (u : ℕ → Set α) : (u 0 ∪ ⋃ i, u (i + 1)) = ⋃ i, u i :=
  sup_iSup_nat_succ u

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