lt_nfpFamily_iff — Mathlib

English

For Small ι, a and b, a < nfpFamily f b iff there exists l with a < List.foldr f b l.

Русский

Для малого множества ι верно: a < nfpFamily f b тогда и только тогда, когда существует список l такой, что a < List.foldr f b l.

LaTeX

$$$[Small\\;ι] \\{a\\;b\\} : a < nfpFamily f b \\iff \\exists l, a < List.foldr f b l$$$

Lean4

theorem lt_nfpFamily_iff [Small.{u} ι] {a b} : a < nfpFamily f b ↔ ∃ l, a < List.foldr f b l :=
  Ordinal.lt_iSup_iff

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