isPWO_sup

Mathlib.Order.WellFoundedSet

URI: https://scilib.ai/kg/mathlib#Finset.isPWO_sup

English

For Preorder α, (s.sup f) is IsPWO iff all f(i) are IsPWO.

Русский

Для предпорядка α, (s.sup f) является IsPWO тогда и только тогда, когда все f(i) являются IsPWO.

LaTeX

$$$(s.sup f).IsPWO \\iff \\forall i \\in s, (f(i)).IsPWO$$$

Lean4

theorem isPWO_sup [Preorder α] (s : Finset ι) {f : ι → Set α} : (s.sup f).IsPWO ↔ ∀ i ∈ s, (f i).IsPWO :=
  s.partiallyWellOrderedOn_sup

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

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

Разделы

Аффилиация

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