iSup_le_succ' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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