iSup_le_succ — Mathlib

English

Let α be a complete lattice and u: ℕ → α. Then ⨆ k ≤ n+1, u(k) = (⨆ k ≤ n, u(k)) ⊔ u(n+1).

Русский

Пусть α — полная решетка, и u: ℕ → α. Тогда верхний предел по k ≤ n+1 равен максимуму верхних пределов по k ≤ n и u(n+1).

LaTeX

$$$\\displaystyle \\big\\vee_{k \\le n+1} u(k) = \\big\\vee_{k \\le n} u(k) \\vee u(n+1).$$$

Lean4

theorem iSup_le_succ (u : ℕ → α) (n : ℕ) : ⨆ k ≤ n + 1, u k = (⨆ k ≤ n, u k) ⊔ u (n + 1) := by
  simp_rw [← Nat.lt_succ_iff, iSup_lt_succ]

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