wellFoundedOn_bUnion — Mathlib

English

For a finite s, the union over i ∈ s of f(i) is WF iff each f(i) is WF.

Русский

Для конечного s объединение по i ∈ s множества f(i) является WF тогда и только тогда, когда каждое f(i) является WF.

LaTeX

$$$(\\\\bigcup_{i \\in s} f(i)).WellFoundedOn\\, r \\iff \\forall i \\in s, (f(i)).WellFoundedOn\\, r$$$

Lean4

@[simp]
theorem wellFoundedOn_bUnion [IsStrictOrder α r] (s : Finset ι) {f : ι → Set α} :
    (⋃ i ∈ s, f i).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r := by
  simpa only [Finset.sup_eq_iSup] using s.wellFoundedOn_sup

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