Theorems · Definition · order theory

DFinsupp.Lex

{ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      (ι → ι → Prop) → ((i : ι) → α i → α i → Prop) → (Π₀ (i : ι), α i) → (Π₀ (i : ι), α i) → Prop

DFinsupp.Lex r s is the lexicographic relation on Π₀ i, α i, where ι is ordered by r, and α i is ordered by s i. The type synonym Lex (Π₀ i, α i) has an order given by DFinsupp.Lex (· < ·) (· < ·), whereas Colex (Π₀ i, α i) has an order given by DFinsupp.Lex (· > ·) (· < ·).

Defined in

Mathlib.Data.DFinsupp.Lex

Cited by

14 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

Zero