le_nfpFamily — Mathlib

English

For any Small ι and f: ι → Ordinal → Ordinal and a, we have a ≤ nfpFamily f a.

Русский

Для любого малого ι и функции f: ι → Ordinal → Ordinal и ординала a выполняется a ≤ nfpFamily f a.

LaTeX

$$$[Small\\;ι]\\ (f:\\iota \\to Ordinal \\to Ordinal)\\ (a:Ordinal)\\; \\; a \\le nfpFamily f a$$$

Lean4

theorem le_nfpFamily [Small.{u} ι] (f : ι → Ordinal.{u} → Ordinal.{u}) (a) : a ≤ nfpFamily f a :=
  foldr_le_nfpFamily f a []

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