no goals
ι : Type u_2
α : Type u_1
β : Type ?u.113342
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Finset ι
f : ι → Set α
⊢ Set.WellFoundedOn (sup ∅ f) r ↔ ∀ (i : ι), i ∈ ∅ → Set.WellFoundedOn (f i) r
simp
no goals
ι : Type u_2
α : Type u_1
β : Type ?u.113342
r : α → α → Prop
inst✝ : IsStrictOrder α r
s✝ : Finset ι
f : ι → Set α
a : ι
s : Finset ι
ha : ¬a ∈ s
hs : Set.WellFoundedOn (sup s f) r ↔ ∀ (i : ι), i ∈ s → Set.WellFoundedOn (f i) r
⊢ Set.WellFoundedOn (sup (cons a s ha) f) r ↔ ∀ (i : ι), i ∈ cons a s ha → Set.WellFoundedOn (f i) r
simp [-sup_set_eq_biUnion, hs]