biSup_ge_eq_iSup — Mathlib

English

Let α be a complete lattice and ι a preordered set. For every function f: ι → α, the supremum over i of the tail supremums sup_{j ≥ i} f(j) equals the supremum of the whole family, i.e. sup_i sup_{j ≥ i} f(j) = sup_i f(i).

Русский

Пусть α — полная решетка, и ι — множество с упорядочиванием. Для любой функции f: ι → α верно, что верхняя граница над i и хвостами sup_{j ≥ i} f(j) суммарно достигает той же величины, что и sup_i f(i).

LaTeX

$$$\\\\bigvee_i \\\\bigvee_{j \\\\ge i} f(j) = \\\\bigvee_i f(i)$$

Lean4

theorem biSup_ge_eq_iSup {ι : Type*} [Preorder ι] {f : ι → α} : ⨆ (i) (j ≥ i), f j = ⨆ i, f i :=
  biSup_le_eq_iSup (ι := ιᵒᵈ)

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