English
Let α be a complete lattice, and u: ℕ → α. Then the supremum over the first n+1 indices equals the supremum over the first n indices joined with the nth term: ⨆ k < n+1, u(k) = (⨆ k < n, u(k)) ⊔ u(n).
Русский
Пусть α — полная решетка, и u: ℕ → α. Тогда верхняя граница над первыми n+1 индексами равна верхней границе над первыми n индексами, объединенной с u(n): ⨆_{k < n+1} u(k) = (⨆_{k < n} u(k)) ⊔ u(n).
LaTeX
$$$\\displaystyle \\big\\vee_{k < n+1} u(k) = \\big(\\big\\vee_{k < n} u(k)\\big) \\vee u(n).$$$
Lean4
theorem iSup_lt_succ (u : ℕ → α) (n : ℕ) : ⨆ k < n + 1, u k = (⨆ k < n, u k) ⊔ u n := by
simp_rw [Nat.lt_add_one_iff, biSup_le_eq_sup]
