biUnion_le_succ'

Mathlib.Data.Nat.Lattice

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

English

Let u: ℕ → Set α and n ∈ ℕ. Then ⋃ k ≤ n+1, u_k = u_0 ∪ ⋃ k ≤ n, u(k+1).

Русский

Пусть u: ℕ → Set α и n ∈ ℕ. Тогда ⋃_{k ≤ n+1} u_k = u_0 ∪ ⋃_{k ≤ n} u_{k+1}.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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