foldr_le_nfpFamily — Mathlib

English

For a small index type ι and function f, a, and list l, List.foldr f a l ≤ nfpFamily f a.

Русский

Для малого множества ι и функций f, a и списка l, List.foldr f a l ≤ nfpFamily f a.

LaTeX

$$$[Small\\;\\iota]\\; (f:\\iota \\to Ordinal \\to Ordinal)\\; (a:\\,Ordinal)\\; (l:\\,List\\,\\iota)\\; \\text{leq}(List.foldr\\; f\\; a\\; l)\\; (nfpFamily\\; f\\; a)$$$

Lean4

theorem foldr_le_nfpFamily [Small.{u} ι] (f : ι → Ordinal.{u} → Ordinal.{u}) (a l) : List.foldr f a l ≤ nfpFamily f a :=
  Ordinal.le_iSup _ _

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