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.order.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
• 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
• β = Π (a : α), β a
@[protected, instance]
def pilex.has_lt {ι : Type u_1} {β : ι → Type u_2} [has_lt ι] [Π (a : ι), has_lt (β a)] :
has_lt (pilex ι β)
Equations
@[protected, instance]
def pilex.inhabited {ι : Type u_1} {β : ι → Type u_2} [Π (a : ι), inhabited (β a)] :
Equations
@[protected, instance]
def pilex.is_strict_order {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [Π (a : ι), partial_order (β a)] :
@[protected, instance]
def pilex.partial_order {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [Π (a : ι), partial_order (β a)] :
Equations
@[protected]
theorem pilex.is_strict_total_order' {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] (wf : well_founded has_lt.lt) [Π (a : ι), linear_order (β a)] :
@[protected]
noncomputable 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
theorem pilex.le_of_forall_le {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] (wf : well_founded has_lt.lt) [Π (a : ι), linear_order (β a)] {a b : β} (h : ∀ (i : ι), a i b i) :
a b
@[protected, instance]
def pilex.ordered_add_comm_group {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [Π (a : ι), ] :
Equations
@[protected, instance]
def pilex.ordered_comm_group {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [Π (a : ι), ordered_comm_group (β a)] :
Equations