iInf_le_succ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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