nfpFamily_le

Mathlib.SetTheory.Ordinal.FixedPoint

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

English

If every List.foldr f a l ≤ b for all lists l, then nfpFamily f a ≤ b.

Русский

Если для каждого списка l выполнено List.foldr f a l ≤ b, то nfpFamily f a ≤ b.

LaTeX

$$$(\\forall l, List.foldr f a l \\le b) \\rightarrow nfpFamily f a \\le b$$$

Lean4

theorem nfpFamily_le {a b} : (∀ l, List.foldr f a l ≤ b) → nfpFamily f a ≤ b :=
  Ordinal.iSup_le

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

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

Разделы

Аффилиация

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