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.

See also #

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 α × β.

source

@[protected, instance]

def pi.lex.inhabited {α : Type u_1} [inhabited α] :

inhabited (lex α)

Equations

pi.lex.inhabited = id

source

@[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 i → x j = y j) ∧ s (x i) (y i)

source

@[simp]

theorem pi.to_lex_apply {ι : Type u_1} {β : ι → Type u_2} (x : Π (i : ι), β i) (i : ι) :

⇑to_lex x i = x i

source

@[simp]

theorem pi.of_lex_apply {ι : Type u_1} {β : ι → Type u_2} (x : lex (Π (i : ι), β i)) (i : ι) :

⇑of_lex x i = x i

source

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

source

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) :

pi.lex r (λ (i : ι), has_lt.lt) x y

source

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)

source

@[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

pi.lex.has_lt = {lt := pi.lex has_lt.lt (λ (_x : ι), has_lt.lt)}

source

@[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

source

@[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

pi.lex.partial_order = partial_order_of_SO has_lt.lt

source

@[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

pi.lex.linear_order = linear_order_of_STO has_lt.lt

source

theorem pi.to_lex_monotone {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [Π (i : ι), partial_order (β i)] :

monotone ⇑to_lex

source

theorem pi.to_lex_strict_mono {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [Π (i : ι), partial_order (β i)] :

strict_mono ⇑to_lex

source

@[simp]

theorem pi.lt_to_lex_update_self_iff {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [Π (i : ι), partial_order (β i)] {x : Π (i : ι), β i} {i : ι} {a : β i} :

⇑to_lex x < ⇑to_lex (function.update x i a) ↔ x i < a

source

@[simp]

theorem pi.to_lex_update_lt_self_iff {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [Π (i : ι), partial_order (β i)] {x : Π (i : ι), β i} {i : ι} {a : β i} :

⇑to_lex (function.update x i a) < ⇑to_lex x ↔ a < x i

source

@[simp]

theorem pi.le_to_lex_update_self_iff {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [Π (i : ι), partial_order (β i)] {x : Π (i : ι), β i} {i : ι} {a : β i} :

⇑to_lex x ≤ ⇑to_lex (function.update x i a) ↔ x i ≤ a

source

@[simp]

theorem pi.to_lex_update_le_self_iff {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [Π (i : ι), partial_order (β i)] {x : Π (i : ι), β i} {i : ι} {a : β i} :

⇑to_lex (function.update x i a) ≤ ⇑to_lex x ↔ a ≤ x i

source

@[protected, instance]

def pi.lex.order_bot {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [Π (a : ι), partial_order (β a)] [Π (a : ι), order_bot (β a)] :

order_bot (lex (Π (a : ι), β a))

Equations

pi.lex.order_bot = {bot := ⇑to_lex ⊥, bot_le := _}

source

@[protected, instance]

def pi.lex.order_top {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [Π (a : ι), partial_order (β a)] [Π (a : ι), order_top (β a)] :

order_top (lex (Π (a : ι), β a))

Equations

pi.lex.order_top = {top := ⇑to_lex ⊤, le_top := _}

source

@[protected, instance]

def pi.lex.bounded_order {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [Π (a : ι), partial_order (β a)] [Π (a : ι), bounded_order (β a)] :

bounded_order (lex (Π (a : ι), β a))

Equations

pi.lex.bounded_order = {top := order_top.top pi.lex.order_top, le_top := _, bot := order_bot.bot pi.lex.order_bot, bot_le := _}

source

@[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))

source

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))

source

@[protected, instance]

def pi.lex.no_max_order {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [nonempty ι] [Π (i : ι), partial_order (β i)] [∀ (i : ι), no_max_order (β i)] :

no_max_order (lex (Π (i : ι), β i))

source

@[protected, instance]

def pi.lex.no_min_order {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [is_well_order ι has_lt.lt] [nonempty ι] [Π (i : ι), partial_order (β i)] [∀ (i : ι), no_min_order (β i)] :

no_min_order (lex (Π (i : ι), β i))

source

@[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

pi.lex.ordered_comm_group = {mul := comm_group.mul pi.comm_group, mul_assoc := _, one := comm_group.one pi.comm_group, one_mul := _, mul_one := _, npow := comm_group.npow pi.comm_group, npow_zero' := _, npow_succ' := _, inv := comm_group.inv pi.comm_group, div := comm_group.div pi.comm_group, div_eq_mul_inv := _, zpow := comm_group.zpow pi.comm_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := partial_order.le pi.lex.partial_order, lt := partial_order.lt pi.lex.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}

source

@[protected, instance]

def pi.lex.ordered_add_comm_group {ι : Type u_1} {β : ι → Type u_2} [linear_order ι] [Π (a : ι), ordered_add_comm_group (β a)] :

ordered_add_comm_group (lex (Π (i : ι), β i))

Equations

pi.lex.ordered_add_comm_group = {add := add_comm_group.add pi.add_comm_group, add_assoc := _, zero := add_comm_group.zero pi.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul pi.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg pi.add_comm_group, sub := add_comm_group.sub pi.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul pi.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := partial_order.le pi.lex.partial_order, lt := partial_order.lt pi.lex.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}

source

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 ∘ ⇑(equiv.swap i j)) < ⇑to_lex f

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