isPWO_bUnion — Mathlib

English

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

Русский

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

LaTeX

$$$(\\\\bigcup i \\in s, f i).IsPWO \\iff \\forall i \\in s, (f i).IsPWO$$$

Lean4

@[simp]
theorem isPWO_bUnion [Preorder α] (s : Finset ι) {f : ι → Set α} : (⋃ i ∈ s, f i).IsPWO ↔ ∀ i ∈ s, (f i).IsPWO :=
  s.partiallyWellOrderedOn_bUnion

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