iInf_le_succ' — Mathlib

English

Let α be a complete lattice and u: ℕ → α. Then iInf_le_succ' := iSup_le_succ' in the order dual; i.e., dual formula for the infimum.

Русский

Пусть α — полная решетка и u: ℕ → α. Тогда формула для нижней границы берется через двойственный порядок: iInf_le_succ' эквивалентно iSup_le_succ' в двойственном порядке.

LaTeX

$$$@\\;\\text{(в двойственном порядке)}\\; \\big\\wedge_{k \\le n+1} u(k) = u(0) \\wedge \\bigwedge_{k \\le n} u(k+1).$$$

Lean4

theorem iInf_le_succ' (u : ℕ → α) (n : ℕ) : ⨅ k ≤ n + 1, u k = u 0 ⊓ ⨅ k ≤ n, u (k + 1) :=
  @iSup_le_succ' αᵒᵈ _ _ _

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