data.pi.lex

# Lexicographic order on Pi types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the lexicographic order for Pi types. a is less than b if a i = b i for all i up to some point k, and a k < b k.

## Notation #

• Πₗ i, α i: Pi type equipped with the lexicographic order. Type synonym of Π i, α i.

Related files are:

• data.finset.colex: Colexicographic order on finite sets.
• data.list.lex: Lexicographic order on lists.
• data.sigma.order: Lexicographic order on Σₗ i, α i.
• data.psigma.order: Lexicographic order on Σₗ' i, α i.
• data.prod.lex: Lexicographic order on α × β.
@[protected, instance]
def pi.lex.inhabited {α : Type u_1} [inhabited α] :
Equations
@[protected]
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 i x j = y j) s (x i) (y i)
@[simp]
theorem pi.to_lex_apply {ι : Type u_1} {β : ι Type u_2} (x : Π (i : ι), β i) (i : ι) :
i = x i
@[simp]
theorem pi.of_lex_apply {ι : Type u_1} {β : ι Type u_2} (x : lex (Π (i : ι), β i)) (i : ι) :
i = x i
theorem pi.lex_lt_of_lt_of_preorder {ι : Type u_1} {β : ι Type u_2} [Π (i : ι), preorder (β i)] {r : ι ι Prop} (hwf : well_founded r) {x y : Π (i : ι), β i} (hlt : x < y) :
(i : ι), ( (j : ι), r j i x j y j y j x j) x i < y i
theorem pi.lex_lt_of_lt {ι : Type u_1} {β : ι Type u_2} [Π (i : ι), partial_order (β i)] {r : ι ι Prop} (hwf : well_founded r) {x y : Π (i : ι), β i} (hlt : x < y) :
(λ (i : ι), has_lt.lt) x y
theorem pi.is_trichotomous_lex {ι : Type u_1} {β : ι Type u_2} (r : ι ι Prop) (s : Π {i : ι}, β i β i Prop) [ (i : ι), is_trichotomous (β i) s] (wf : well_founded r) :
is_trichotomous (Π (i : ι), β i) (pi.lex r s)
@[protected, instance]
def pi.lex.has_lt {ι : Type u_1} {β : ι Type u_2} [has_lt ι] [Π (a : ι), has_lt (β a)] :
has_lt (lex (Π (i : ι), β i))
Equations
@[protected, instance]
def pi.lex.is_strict_order {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (a : ι), partial_order (β a)] :
is_strict_order (lex (Π (i : ι), β i)) has_lt.lt
@[protected, instance]
def pi.lex.partial_order {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (a : ι), partial_order (β a)] :
partial_order (lex (Π (i : ι), β i))
Equations
@[protected, instance]
noncomputable def pi.lex.linear_order {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (a : ι), linear_order (β a)] :
linear_order (lex (Π (i : ι), β i))

Πₗ i, α i is a linear order if the original order is well-founded.

Equations
theorem pi.to_lex_monotone {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (i : ι), partial_order (β i)] :
theorem pi.to_lex_strict_mono {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (i : ι), partial_order (β i)] :
@[simp]
theorem pi.lt_to_lex_update_self_iff {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (i : ι), partial_order (β i)] {x : Π (i : ι), β i} {i : ι} {a : β i} :
< to_lex i a) x i < a
@[simp]
theorem pi.to_lex_update_lt_self_iff {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (i : ι), partial_order (β i)] {x : Π (i : ι), β i} {i : ι} {a : β i} :
to_lex i a) < a < x i
@[simp]
theorem pi.le_to_lex_update_self_iff {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (i : ι), partial_order (β i)] {x : Π (i : ι), β i} {i : ι} {a : β i} :
to_lex i a) x i a
@[simp]
theorem pi.to_lex_update_le_self_iff {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (i : ι), partial_order (β i)] {x : Π (i : ι), β i} {i : ι} {a : β i} :
to_lex i a) a x i
@[protected, instance]
def pi.lex.order_bot {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (a : ι), partial_order (β a)] [Π (a : ι), order_bot (β a)] :
order_bot (lex (Π (a : ι), β a))
Equations
@[protected, instance]
def pi.lex.order_top {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (a : ι), partial_order (β a)] [Π (a : ι), order_top (β a)] :
order_top (lex (Π (a : ι), β a))
Equations
@[protected, instance]
def pi.lex.bounded_order {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (a : ι), partial_order (β a)] [Π (a : ι), bounded_order (β a)] :
bounded_order (lex (Π (a : ι), β a))
Equations
@[protected, instance]
def pi.lex.densely_ordered {ι : Type u_1} {β : ι Type u_2} [preorder ι] [Π (i : ι), has_lt (β i)] [ (i : ι), densely_ordered (β i)] :
densely_ordered (lex (Π (i : ι), β i))
theorem pi.lex.no_max_order' {ι : Type u_1} {β : ι Type u_2} [preorder ι] [Π (i : ι), has_lt (β i)] (i : ι) [no_max_order (β i)] :
no_max_order (lex (Π (i : ι), β i))
@[protected, instance]
def pi.lex.no_max_order {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [nonempty ι] [Π (i : ι), partial_order (β i)] [ (i : ι), no_max_order (β i)] :
no_max_order (lex (Π (i : ι), β i))
@[protected, instance]
def pi.lex.no_min_order {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [nonempty ι] [Π (i : ι), partial_order (β i)] [ (i : ι), no_min_order (β i)] :
no_min_order (lex (Π (i : ι), β i))
@[protected, instance]
def pi.lex.ordered_comm_group {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (a : ι), ordered_comm_group (β a)] :
ordered_comm_group (lex (Π (i : ι), β i))
Equations
@[protected, instance]
def pi.lex.ordered_add_comm_group {ι : Type u_1} {β : ι Type u_2} [linear_order ι] [Π (a : ι), ] :
ordered_add_comm_group (lex (Π (i : ι), β i))
Equations
theorem pi.lex_desc {ι : Type u_1} {α : Type u_2} [preorder ι] [decidable_eq ι] [preorder α] {f : ι α} {i j : ι} (h₁ : i < j) (h₂ : f j < f i) :
to_lex (f j)) <

If we swap two strictly decreasing values in a function, then the result is lexicographically smaller than the original function.