partialSups_apply — Mathlib

English

For a function f: ι → α and an index i, the i-th value of partialSups f is the supremum of f over the initial segment { j | j ≤ i }.

Русский

Для функции f: ι → α и индекса i значение partialSups f на позиции i равно наибольшему элементу множества { f(j) | j ≤ i }.

LaTeX

$$$(\\partialSups f)(i) = \\sup_{j \\le i} f(j)$$$

Lean4

theorem partialSups_apply (f : ι → α) (i : ι) : partialSups f i = (Iic i).sup' nonempty_Iic f :=
  rfl

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