no goals
ι : Type u_1
α : Type u_2
β : Type ?u.125092
r : α → α → Prop
s : Finset ι
f : ι → Set α
⊢ Set.PartiallyWellOrderedOn (⋃ (i : ι) (_ : i ∈ s), f i) r ↔ ∀ (i : ι), i ∈ s → Set.PartiallyWellOrderedOn (f i) r
simpa only [Finset.sup_eq_iSup] using s.partiallyWellOrderedOn_sup