Theorems · Theorem · order theory

Finset.wellFoundedOn_bUnion

∀ {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] (s : Finset ι) {f : ι → Set α},
  (⋃ i ∈ s, f i).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r

Defined in

Mathlib.Order.WellFoundedSet

Cited by

1 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

IsStrictOrder