English
For f: ι → α, the sequence i ↦ sup { f(j) | j ≤ i } defines a monotone sequence when α is a semilattice with supremum and ι is ordered suitably.
Русский
Для функций f: ι → α, последовательность i ↦ sup{ f(j) | j ≤ i } является монотонной при условии, что α образует полуупорядоченную полную сумму и ι обладает подходящим порядком.
LaTeX
$$$\\mathrm{Monotone}\\big( i \\mapsto \\sup_{j \\le i} f(j) \\big)$$$
Lean4
/-- The monotone sequence whose value at `i` is the supremum of the `f j` where `j ≤ i`. -/
def partialSups (f : ι → α) : ι →o α where
toFun i := (Iic i).sup' nonempty_Iic f
monotone' _ _ hmn := sup'_mono f (Iic_subset_Iic.mpr hmn) nonempty_Iic
