isWF_bUnion — Mathlib

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

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