mathlib documentation

data.psigma.order

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 #

See also #

Related files are:

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} [partial_order ι] [Π (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