data.sigma.order

# Orders on a sigma type #

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

This file defines two orders on a sigma type:

• The disjoint sum of orders. a is less b iff a and b are in the same summand and a is less than b there.
• The lexicographical order. 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.

We make the disjoint sum of orders the default set of instances. The lexicographic order goes on a type synonym.

## Notation #

• Σₗ i, α i: Sigma 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.pi.lex: Lexicographic order on Πₗ i, α i.
• data.psigma.order: Lexicographic order on Σₗ' i, α i. Basically a twin of this file.
• data.prod.lex: Lexicographic order on α × β.

## TODO #

Upgrade equiv.sigma_congr_left, equiv.sigma_congr, equiv.sigma_assoc, equiv.sigma_prod_of_equiv, equiv.sigma_equiv_prod, ... to order isomorphisms.

### Disjoint sum of orders on sigma#

inductive sigma.le {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_le (α i)] (a b : Σ (i : ι), α i) :
Prop

Disjoint sum of orders. ⟨i, a⟩ ≤ ⟨j, b⟩ iff i = j and a ≤ b.

inductive sigma.lt {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_lt (α i)] (a b : Σ (i : ι), α i) :
Prop

Disjoint sum of orders. ⟨i, a⟩ < ⟨j, b⟩ iff i = j and a < b.

@[protected, instance]
def sigma.has_le {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_le (α i)] :
has_le (Σ (i : ι), α i)
Equations
@[protected, instance]
def sigma.has_lt {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_lt (α i)] :
has_lt (Σ (i : ι), α i)
Equations
@[simp]
theorem sigma.mk_le_mk_iff {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_le (α i)] {i : ι} {a b : α i} :
i, a⟩ i, b⟩ a b
@[simp]
theorem sigma.mk_lt_mk_iff {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_lt (α i)] {i : ι} {a b : α i} :
i, a⟩ < i, b⟩ a < b
theorem sigma.le_def {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_le (α i)] {a b : Σ (i : ι), α i} :
a b (h : a.fst = b.fst), eq.rec a.snd h b.snd
theorem sigma.lt_def {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_lt (α i)] {a b : Σ (i : ι), α i} :
a < b (h : a.fst = b.fst), eq.rec a.snd h < b.snd
@[protected, instance]
def sigma.preorder {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] :
preorder (Σ (i : ι), α i)
Equations
@[protected, instance]
def sigma.partial_order {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), partial_order (α i)] :
partial_order (Σ (i : ι), α i)
Equations
@[protected, instance]
def sigma.densely_ordered {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] [ (i : ι), densely_ordered (α i)] :
densely_ordered (Σ (i : ι), α i)

### Lexicographical order on sigma#

@[protected, instance]
def sigma.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 sigma.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
theorem sigma.lex.le_def {ι : Type u_1} {α : ι Type u_2} [has_lt ι] [Π (i : ι), has_le (α i)] {a b : Σₗ (i : ι), α i} :
a b a.fst < b.fst (h : a.fst = b.fst), eq.rec a.snd h b.snd
theorem sigma.lex.lt_def {ι : Type u_1} {α : ι Type u_2} [has_lt ι] [Π (i : ι), has_lt (α i)] {a b : Σₗ (i : ι), α i} :
a < b a.fst < b.fst (h : a.fst = b.fst), eq.rec a.snd h < b.snd
@[protected, instance]
def sigma.lex.preorder {ι : Type u_1} {α : ι Type u_2} [preorder ι] [Π (i : ι), preorder (α i)] :
preorder (Σₗ (i : ι), α i)

The lexicographical preorder on a sigma type.

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

The lexicographical partial order on a sigma type.

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

The lexicographical linear order on a sigma type.

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