nfpFamily_le_iff

Mathlib.SetTheory.Ordinal.FixedPoint

URI: https://scilib.ai/kg/mathlib#Ordinal.nfpFamily_le_iff

English

For Small ι, (nfpFamily f a) ≤ b iff ∀ l, List.foldr f a l ≤ b.

Русский

Для малого ι: nfpFamily f a ≤ b эквивалентно ∀ l, List.foldr f a l ≤ b.

LaTeX

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

Lean4

theorem nfpFamily_le_iff [Small.{u} ι] {a b} : nfpFamily f a ≤ b ↔ ∀ l, List.foldr f a l ≤ b :=
  Ordinal.iSup_le_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru