mathlib documentation

order.pilex

def pi.lex {ι : Type u_1} {β : ι → Type u_2} :
(ι → ι → Prop)(Π {i : ι}, β iβ i → Prop)(Π (i : ι), β i)(Π (i : ι), β i) → Prop

The lexicographic relation on Π i : ι, β i, where ι is ordered by r, and each β i is ordered by s.

Equations
  • pi.lex r s x y = ∃ (i : ι), (∀ (j : ι), r j ix j = y j) s (x i) (y i)
def pilex (α : Type u_1) :
(α → Type u_2)Type (max u_1 u_2)

The cartesian product of an indexed family, equipped with the lexicographic order.

Equations
  • pilex α β = Π (a : α), β a
@[instance]
def pilex.has_lt {ι : Type u_1} {β : ι → Type u_2} [has_lt ι] [Π (a : ι), has_lt (β a)] :
has_lt (pilex ι β)

Equations
@[instance]
def pilex.inhabited {ι : Type u_1} {β : ι → Type u_2} [Π (a : ι), inhabited (β a)] :

Equations
@[instance]
def pilex.partial_order {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [Π (a : ι), partial_order (β a)] :

Equations
def pilex.linear_order {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] (wf : well_founded has_lt.lt) [Π (a : ι), linear_order (β a)] :

pilex is a linear order if the original order is well-founded. This cannot be an instance, since it depends on the well-foundedness of <.

Equations