isWF_sup — Mathlib

English

For any Finset s and family of sets f, (s.sup f) is WF iff each f(i) is WF.

Русский

Для любого Finset s и семейства множеств f, (s.sup f) является WF тогда и только тогда, когда каждое f(i) является WF.

LaTeX

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

Lean4

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

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