mathlib documentation

data.pi.lex

Lexicographic order on Pi types #

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 #

See also #

Related files are:

@[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
  • pi.lex r s x y = ∃ (i : ι), (∀ (j : ι), r j ix j = y j) s (x i) (y i)
@[simp]
theorem pi.to_lex_apply {ι : Type u_1} {β : ι → Type u_2} (x : Π (i : ι), β i) (i : ι) :
to_lex x i = x i
@[simp]
theorem pi.of_lex_apply {ι : Type u_1} {β : ι → Type u_2} (x : lex (Π (i : ι), β i)) (i : ι) :
of_lex x i = x i
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 ι] [is_well_order ι has_lt.lt] [Π (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.lex.le_of_forall_le {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [Π (a : ι), linear_order (β a)] {a b : lex (Π (i : ι), β i)} (h : ∀ (i : ι), a i b i) :
a b
theorem pi.lex.le_of_of_lex_le {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [Π (a : ι), linear_order (β a)] {a b : lex (Π (i : ι), β i)} (h : of_lex a of_lex b) :
a b
theorem pi.to_lex_monotone {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [Π (a : ι), linear_order (β a)] :
@[protected, instance]
def pi.lex.order_bot {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [Π (a : ι), linear_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 ι] [is_well_order ι has_lt.lt] [Π (a : ι), linear_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 ι] [is_well_order ι has_lt.lt] [Π (a : ι), linear_order (β a)] [Π (a : ι), bounded_order (β a)] :
bounded_order (lex (Π (a : ι), β a))
Equations