English
For a finite s, the big union over i, h of f(i) is WF iff each f(i) is WF.
Русский
Для конечного s объединение по i ∈ s и по вложенным индексам h множества f(i) является WF тогда и только тогда, когда каждое f(i) является WF.
LaTeX
$$$(\\\\bigcup i \\in s,\\\\, f(i)).IsWF \\iff \\forall i \\in s, (f(i)).IsWF$$$
Lean4
@[simp]
theorem isWF_bUnion [Preorder α] (s : Finset ι) {f : ι → Set α} : (⋃ i ∈ s, f i).IsWF ↔ ∀ i ∈ s, (f i).IsWF :=
s.wellFoundedOn_bUnion