Finite unions of partially well-ordered sets #
A union indexed by a finite type is partially well ordered when every member is. This is the finite-family form of closure of partially well-ordered subsets of a linear order under union.
theorem
Set.IsPWO.iUnion_of_finite
{α : Type u}
{ι : Type v}
[LinearOrder α]
[Finite ι]
(S : ι → Set α)
(hS : ∀ (i : ι), (S i).IsPWO)
:
(⋃ (i : ι), S i).IsPWO
A finite union of partially well-ordered sets is partially well ordered.