# mathlib3documentation

data.psigma.order

# Lexicographic order on a sigma type #

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

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.

Related files are:

• data.finset.colex: Colexicographic order on finite sets.
• data.list.lex: Lexicographic order on lists.
• data.pi.lex: Lexicographic order on Πₗ i, α i.
• data.sigma.order: Lexicographic order on Σₗ i, α i. Basically a twin of this file.
• data.prod.lex: 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
@[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
@[protected, instance]
def psigma.lex.preorder {ι : Type u_1} {α : ι Type u_2} [preorder ι] [Π (i : ι), preorder (α i)] :
preorder (Σₗ' (i : ι), α i)
Equations
@[protected, instance]
def psigma.lex.partial_order {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), partial_order (α i)] :
partial_order (Σₗ' (i : ι), α i)

Dictionary / lexicographic partial_order for dependent pairs.

Equations
@[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
@[protected, instance]
def psigma.lex.order_bot {ι : Type u_1} {α : ι Type u_2} [order_bot ι] [Π (i : ι), preorder (α i)] [order_bot )] :
order_bot (Σₗ' (i : ι), α i)

The lexicographical linear order on a sigma type.

Equations
@[protected, instance]
def psigma.lex.order_top {ι : Type u_1} {α : ι Type u_2} [order_top ι] [Π (i : ι), preorder (α i)] [order_top )] :
order_top (Σₗ' (i : ι), α i)

The lexicographical linear order on a sigma type.

Equations
@[protected, instance]
def psigma.lex.bounded_order {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] [order_bot )] [order_top )] :
bounded_order (Σₗ' (i : ι), α i)

The lexicographical linear order on a sigma type.

Equations
@[protected, instance]
def psigma.lex.densely_ordered {ι : Type u_1} {α : ι Type u_2} [preorder ι] [ (i : ι), nonempty (α i)] [Π (i : ι), preorder (α i)] [ (i : ι), densely_ordered (α i)] :
densely_ordered (Σₗ' (i : ι), α i)
@[protected, instance]
def psigma.lex.densely_ordered_of_no_max_order {ι : Type u_1} {α : ι Type u_2} [preorder ι] [Π (i : ι), preorder (α i)] [ (i : ι), densely_ordered (α i)] [ (i : ι), no_max_order (α i)] :
densely_ordered (Σₗ' (i : ι), α i)
@[protected, instance]
def psigma.lex.densely_ordered_of_no_min_order {ι : Type u_1} {α : ι Type u_2} [preorder ι] [Π (i : ι), preorder (α i)] [ (i : ι), densely_ordered (α i)] [ (i : ι), no_min_order (α i)] :
densely_ordered (Σₗ' (i : ι), α i)
@[protected, instance]
def psigma.lex.no_max_order_of_nonempty {ι : Type u_1} {α : ι Type u_2} [preorder ι] [Π (i : ι), preorder (α i)] [no_max_order ι] [ (i : ι), nonempty (α i)] :
no_max_order (Σₗ' (i : ι), α i)
@[protected, instance]
def psigma.lex.no_min_order_of_nonempty {ι : Type u_1} {α : ι Type u_2} [preorder ι] [Π (i : ι), preorder (α i)] [no_max_order ι] [ (i : ι), nonempty (α i)] :
no_max_order (Σₗ' (i : ι), α i)
@[protected, instance]
def psigma.lex.no_max_order {ι : Type u_1} {α : ι Type u_2} [preorder ι] [Π (i : ι), preorder (α i)] [ (i : ι), no_max_order (α i)] :
no_max_order (Σₗ' (i : ι), α i)
@[protected, instance]
def psigma.lex.no_min_order {ι : Type u_1} {α : ι Type u_2} [preorder ι] [Π (i : ι), preorder (α i)] [ (i : ι), no_min_order (α i)] :
no_min_order (Σₗ' (i : ι), α i)