biSup_lt_eq_iSup — Mathlib

English

If the index set is linearly ordered with a least upper bound property, the supremum of i with all j < i of f(j) equals the supremum of f.

Русский

При линейном порядке индексов и существовании наибольшего верхнего предела, супремум по i и j< i f(j) равен супремуму f.

LaTeX

$$$ \\sup_{i} \\sup_{j < i} f(j) = \\sup_{i} f(i). $$$

Lean4

theorem biSup_lt_eq_iSup {ι : Type*} [LT ι] [NoMaxOrder ι] {f : ι → α} : ⨆ (i) (j < i), f j = ⨆ i, f i :=
  by
  apply le_antisymm
  · exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _
  · refine iSup_le fun j ↦ ?_
    obtain ⟨i, jlt⟩ := exists_gt j
    exact le_iSup_of_le i (le_iSup₂_of_le j jlt le_rfl)

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