foldr_strictMono — Mathlib

English

If every a ↦ f a is strictly monotone, then the right fold is strictly monotone in its result.

Русский

Если для каждого a функция f a строго монотонна, то правый сверток монотонен строгим образом.

LaTeX

$$$[Preorder \\beta] {f : \\alpha \\to \\beta \\to \\beta} (H : \\forall a, StrictMono (f a)) (l : List \\alpha) : StrictMono (\\lambda b, List.foldr f b l)$$$

Lean4

theorem foldr_strictMono [Preorder β] {f : α → β → β} (H : ∀ a, StrictMono (f a)) (l : List α) :
    StrictMono fun b ↦ l.foldr f b := fun _ _ h ↦ List.recOn l h fun i _ hl ↦ H i hl

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