sup_iSup_nat_succ — Mathlib

English

For a sequence u: ℕ → α, the join of u(0) with the tail ⨆ i, u(i+1) equals the whole supremum ⨆ i, u(i): u(0) ∨ (sup_{i} u(i+1)) = sup_{i} u(i).

Русский

Для последовательности u: ℕ → α, объединение u(0) с хвостом ⨆ i, u(i+1) даёт всю верхнюю грань: u(0) ∨ (sup_{i} u(i+1)) = sup_{i} u(i).

LaTeX

$$$u(0) \lor \Bigl(\sup_{i} u(i+1)\Bigr) = \sup_{i} u(i)$$$

Lean4

theorem sup_iSup_nat_succ (u : ℕ → α) : (u 0 ⊔ ⨆ i, u (i + 1)) = ⨆ i, u i :=
  calc
    (u 0 ⊔ ⨆ i, u (i + 1)) = ⨆ x ∈ {0} ∪ range Nat.succ, u x := by { rw [iSup_union, iSup_singleton, iSup_range]
    }
    _ = ⨆ i, u i := by rw [Nat.zero_union_range_succ, iSup_univ]

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