partiallyWellOrderedOn_bUnion — Mathlib

English

For a finite s, (⋃ i ∈ s, f i) is PW0 iff all f(i) are PW0.

Русский

Для конечного s объединение ⋃ i ∈ s, f(i) частично хорошо упорядочено тогда и только тогда, когда каждое f(i) частично хорошо упорядочено.

LaTeX

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

Lean4

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

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