iInf_lt_succ — Mathlib

English

Let α be a complete lattice and u: ℕ → α. Then iInf over k < n+1 equals iInf over k < n with a meet at n: ⨅ k < n+1, u(k) = (⨅ k < n, u(k)) ⊓ u(n).

Русский

Пусть α — полная решетка и u: ℕ → α. Тогда ∧ по k < n+1 u(k) = (∧ по k < n u(k)) ∧ u(n).

LaTeX

$$$\\displaystyle \\big\\wedge_{k < n+1} u(k) = \\left(\\big\\wedge_{k < n} u(k)\\right) \\wedge u(n).$$$

Lean4

theorem iInf_lt_succ (u : ℕ → α) (n : ℕ) : ⨅ k < n + 1, u k = (⨅ k < n, u k) ⊓ u n :=
  @iSup_lt_succ αᵒᵈ _ _ _

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