Lexicographic order on a sigma type #
This file defines the lexicographic order on Σₗ' i, α i. a is less than b if its summand is
strictly less than the summand of b or they are in the same summand and a is less than b
there.
Notation #
Σₗ' i, α i: Sigma type equipped with the lexicographic order. A 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. Basically a twin of this file.order.lexicographic: Lexicographic order onα × β.
TODO #
Define the disjoint order on Σ' i, α i, where x ≤ y only if x.fst = y.fst.
Prove that a sigma type is a no_max_order, no_min_order, densely_ordered when its summands
are.
@[protected, instance]
def
psigma.lex.has_le
{ι : Type u_1}
{α : ι → Type u_2}
[has_lt ι]
[Π (i : ι), has_le (α i)] :
has_le (Σₗ' (i : ι), α i)
The lexicographical ≤ on a sigma type.
Equations
- psigma.lex.has_le = {le := psigma.lex has_lt.lt (λ (i : ι), has_le.le)}
@[protected, instance]
def
psigma.lex.has_lt
{ι : Type u_1}
{α : ι → Type u_2}
[has_lt ι]
[Π (i : ι), has_lt (α i)] :
has_lt (Σₗ' (i : ι), α i)
The lexicographical < on a sigma type.
Equations
- psigma.lex.has_lt = {lt := psigma.lex has_lt.lt (λ (i : ι), has_lt.lt)}
@[protected, instance]
def
psigma.lex.preorder
{ι : Type u_1}
{α : ι → Type u_2}
[preorder ι]
[Π (i : ι), preorder (α i)] :
preorder (Σₗ' (i : ι), α i)
Equations
- psigma.lex.preorder = {le := has_le.le psigma.lex.has_le, lt := has_lt.lt psigma.lex.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
@[protected, instance]
def
psigma.lex.partial_order
{ι : Type u_1}
{α : ι → Type u_2}
[partial_order ι]
[Π (i : ι), partial_order (α i)] :
partial_order (Σₗ' (i : ι), α i)
Dictionary / lexicographic partial_order for dependent pairs.
Equations
- psigma.lex.partial_order = {le := preorder.le psigma.lex.preorder, lt := preorder.lt psigma.lex.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[protected, instance]
def
psigma.lex.linear_order
{ι : Type u_1}
{α : ι → Type u_2}
[linear_order ι]
[Π (i : ι), linear_order (α i)] :
linear_order (Σₗ' (i : ι), α i)
Dictionary / lexicographic linear_order for pairs.
Equations
- psigma.lex.linear_order = {le := partial_order.le psigma.lex.partial_order, lt := partial_order.lt psigma.lex.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := psigma.lex.decidable has_lt.lt (λ (i : ι), has_le.le) (λ (i : ι) (a b : (λ (i : ι), (λ (i : ι), (λ (i : ι), α i) i) i) i), has_le.le.decidable a b), decidable_eq := psigma.decidable_eq (λ (a : ι) (a_1 b : α a), eq.decidable a_1 b), decidable_lt := psigma.lex.decidable has_lt.lt (λ (i : ι), has_lt.lt) (λ (i : ι) (a b : (λ (i : ι), (λ (i : ι), (λ (i : ι), α i) i) i) i), has_lt.lt.decidable a b), max := max_default (λ (a b : Σₗ' (i : ι), α i), psigma.lex.decidable has_lt.lt (λ (i : ι), has_le.le) a b), max_def := _, min := min_default (λ (a b : Σₗ' (i : ι), α i), psigma.lex.decidable has_lt.lt (λ (i : ι), has_le.le) a b), min_def := _}