iSup_lt_succ' — Mathlib

English

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

Русский

Пусть α — полная решетка, и u: ℕ → α. Тогда \$\\big\\vee_{k < n+1} u(k) = u(0) \\vee \\big\\vee_{k < n} u(k+1).\$

LaTeX

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

Lean4

theorem iSup_lt_succ' (u : ℕ → α) (n : ℕ) : ⨆ k < n + 1, u k = u 0 ⊔ ⨆ k < n, u (k + 1) :=
  by
  rw [← sup_iSup_nat_succ]
  simp

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