nfpFamily_monotone — Mathlib

English

If each f_i is monotone, then the function a ↦ nfpFamily f a is monotone.

Русский

Если каждый f_i монотонна, то функция a ↦ nfpFamily f a монотонна.

LaTeX

$$$[Small\\;ι] (\\forall i, Monotone(f i)) \\rightarrow Monotone(nfpFamily f)$$$

Lean4

theorem nfpFamily_monotone [Small.{u} ι] (hf : ∀ i, Monotone (f i)) : Monotone (nfpFamily f) := fun _ _ h ↦
  nfpFamily_le <| fun l ↦ (List.foldr_monotone hf l h).trans (foldr_le_nfpFamily _ _ l)

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