biSup_le_eq_iSup — Mathlib

English

In a preordered setting, the supremum of i and a bound is equal to the supremum over i of iSup with a bound included.

Русский

В предорядке верхний предел равен верхнему пределу с учётом ограничителя.

LaTeX

$$$ \\bigvee_{i} f(i) \\le \\bigvee_{i} f(i) ,$$$

Lean4

theorem biSup_le_eq_iSup {ι : Type*} [Preorder ι] {f : ι → α} : ⨆ (i) (j ≤ i), f j = ⨆ i, f i :=
  by
  apply le_antisymm
  · exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _
  · exact iSup_le fun j ↦ le_iSup_of_le j (le_iSup₂_of_le j le_rfl le_rfl)

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