mathlib documentation

order.pilex

Lexicographic order on Pi types #

This file defines the lexicographic relation for Pi types of partial orders and linear orders. We also provide a pilex analog of pi.ordered_comm_group (see algebra.ordered_pi).

def pi.lex {ι : Type u_1} {β : ι → Type u_2} (r : ι → ι → Prop) (s : Π {i : ι}, β iβ i → Prop) (x y : Π (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
@[instance]
def pilex.ordered_add_comm_group {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [Π (a : ι), ordered_add_comm_group (β a)] :