iInf_lt_succ' — Mathlib

English

Let α be a complete lattice, and u: ℕ → α. Then iInf over k < n+1 equals iSup over k ≤ n of u(k) with a dual adjustment: iInf_lt_succ' = iSup_lt_succ' in dual, i.e., iInf_lt_succ'(u,n) := iSup_lt_succ'(u,n) in the order dual.

Русский

Пусть α — полная решетка, и u: ℕ → α. Тогда iInf над k < n+1 равен iSup над k ≤ n через двойственный порядок, то есть эквивалентно формуле с двойственным порядком.

LaTeX

$$$\\big\\wedge_{k < n+1} u(k) = u(0) \\;\\sqcap\\; \\big\\wedge_{k < n} u(k+1).$$$

Lean4

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

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