data.sigma.order

# Orders on a sigma type #

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.

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 #

Prove that a sigma type is a no_max_order, no_min_order, densely_ordered when its summands are.

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
• fiber : ∀ {ι : Type u_1} {α : ι → Type u_2} [_inst_1 : Π (i : ι), has_le (α i)] (i : ι) (a b : α i), a bi, a⟩.le i, b⟩

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
• fiber : ∀ {ι : Type u_1} {α : ι → Type u_2} [_inst_1 : Π (i : ι), has_lt (α i)] (i : ι) (a b : α i), a < bi, a⟩.lt i, b⟩

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

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