no goals
ι : Type u_2
α : Type u_1
β : Type ?u.124371
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Finset ι
f : ι → Set α
⊢ Set.WellFoundedOn (⋃ (i : ι) (_ : i ∈ s), f i) r ↔ ∀ (i : ι), i ∈ s → Set.WellFoundedOn (f i) r
simpa only [Finset.sup_eq_iSup] using s.wellFoundedOn_sup