biUnion_le_succ — Mathlib

English

For u: ℕ → Set α and n ∈ ℕ, the union over k ≤ n+1 equals the union over k ≤ n together with u(n+1): ⋃ k ≤ n+1, u_k = (⋃ k ≤ n, u_k) ∪ u(n+1).

Русский

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

LaTeX

$$$\\displaystyle \\bigcup_{k \\le n+1} u(k) = \\bigcup_{k \\le n} u(k) \\cup u(n+1).$$$

Lean4

theorem biUnion_le_succ (u : ℕ → Set α) (n : ℕ) : ⋃ k ≤ n + 1, u k = (⋃ k ≤ n, u k) ∪ u (n + 1) :=
  Nat.iSup_le_succ u n

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