Theorems · Theorem · order theory

Pi.Lex.wellFounded

∀ {ι : Type u_1} {α : ι → Type u_2} (r : ι → ι → Prop) {s : (i : ι) → α i → α i → Prop} [IsStrictTotalOrder ι r]
  [Finite ι], (∀ (i : ι), WellFounded (s i)) → WellFounded (Pi.Lex r fun {i} => s i)

Defined in

Mathlib.Data.DFinsupp.WellFounded

Cited by

2 results in Mathlib

Foundations

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

Assumes

IsStrictTotalOrderFinite