# Documentation

Mathlib.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 #

• _root_.Lex (Sigma α): 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 #

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} [inst : (i : ι) → LE (α i)] (_a : (i : ι) × α i) (_b : (i : ι) × α i) :
• fiber: ∀ {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → LE (α i)] (i : ι) (a b : α i), a bSigma.le { fst := i, snd := a } { fst := i, snd := b }

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

Instances For
inductive Sigma.lt {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → LT (α i)] (_a : (i : ι) × α i) (_b : (i : ι) × α i) :
• fiber: ∀ {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → LT (α i)] (i : ι) (a b : α i), a < bSigma.lt { fst := i, snd := a } { fst := i, snd := b }

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

Instances For
instance Sigma.LE {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → LE (α i)] :
LE ((i : ι) × α i)
Equations
• Sigma.LE = { le := Sigma.le }
instance Sigma.LT {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → LT (α i)] :
LT ((i : ι) × α i)
Equations
• Sigma.LT = { lt := Sigma.lt }
@[simp]
theorem Sigma.mk_le_mk_iff {ι : Type u_2} {α : ιType u_1} [inst : (i : ι) → LE (α i)] {i : ι} {a : α i} {b : α i} :
{ fst := i, snd := a } { fst := i, snd := b } a b
@[simp]
theorem Sigma.mk_lt_mk_iff {ι : Type u_2} {α : ιType u_1} [inst : (i : ι) → LT (α i)] {i : ι} {a : α i} {b : α i} :
{ fst := i, snd := a } < { fst := i, snd := b } a < b
theorem Sigma.le_def {ι : Type u_2} {α : ιType u_1} [inst : (i : ι) → LE (α i)] {a : (i : ι) × α i} {b : (i : ι) × α i} :
a b h, ha.snd b.snd
theorem Sigma.lt_def {ι : Type u_2} {α : ιType u_1} [inst : (i : ι) → LT (α i)] {a : (i : ι) × α i} {b : (i : ι) × α i} :
a < b h, ha.snd < b.snd
instance Sigma.preorder {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → Preorder (α i)] :
Preorder ((i : ι) × α i)
Equations
• Sigma.preorder = let src := Sigma.LE; let src_1 := Sigma.LT; Preorder.mk (_ : ∀ (x : (i : ι) × α i), x x) (_ : ∀ (a b c : (i : ι) × α i), a bb ca c)
instance Sigma.instPartialOrderSigma {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → PartialOrder (α i)] :
PartialOrder ((i : ι) × α i)
Equations
• Sigma.instPartialOrderSigma = let src := Sigma.preorder; PartialOrder.mk (_ : ∀ (a b : (i : ι) × α i), a bb aa = b)
instance Sigma.instDenselyOrderedSigmaLTToLT {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → Preorder (α i)] [inst : ∀ (i : ι), DenselyOrdered (α i)] :
DenselyOrdered ((i : ι) × α i)
Equations

### Lexicographical order on Sigma#

The notation Σₗ i, α i refers to a sigma type equipped with the lexicographic order.

Equations
• One or more equations did not get rendered due to their size.
instance Sigma.Lex.LE {ι : Type u_1} {α : ιType u_2} [inst : LT ι] [inst : (i : ι) → LE (α i)] :
LE (Lex ((i : ι) × α i))

The lexicographical ≤≤ on a sigma type.

Equations
• Sigma.Lex.LE = { le := Sigma.Lex (fun x x_1 => x < x_1) fun x x_1 x_2 => x_1 x_2 }
instance Sigma.Lex.LT {ι : Type u_1} {α : ιType u_2} [inst : LT ι] [inst : (i : ι) → LT (α i)] :
LT (Lex ((i : ι) × α i))

The lexicographical < on a sigma type.

Equations
• Sigma.Lex.LT = { lt := Sigma.Lex (fun x x_1 => x < x_1) fun x x_1 x_2 => x_1 < x_2 }
theorem Sigma.Lex.le_def {ι : Type u_1} {α : ιType u_2} [inst : LT ι] [inst : (i : ι) → LE (α i)] {a : Lex ((i : ι) × α i)} {b : Lex ((i : ι) × α i)} :
a b a.fst < b.fst h, ha.snd b.snd
theorem Sigma.Lex.lt_def {ι : Type u_1} {α : ιType u_2} [inst : LT ι] [inst : (i : ι) → LT (α i)] {a : Lex ((i : ι) × α i)} {b : Lex ((i : ι) × α i)} :
a < b a.fst < b.fst h, ha.snd < b.snd
instance Sigma.Lex.preorder {ι : Type u_1} {α : ιType u_2} [inst : ] [inst : (i : ι) → Preorder (α i)] :
Preorder (Lex ((i : ι) × α i))

The lexicographical preorder on a sigma type.

Equations
• One or more equations did not get rendered due to their size.
instance Sigma.Lex.partialOrder {ι : Type u_1} {α : ιType u_2} [inst : ] [inst : (i : ι) → PartialOrder (α i)] :
PartialOrder (Lex ((i : ι) × α i))

The lexicographical partial order on a sigma type.

Equations
• One or more equations did not get rendered due to their size.
instance Sigma.Lex.linearOrder {ι : Type u_1} {α : ιType u_2} [inst : ] [inst : (i : ι) → LinearOrder (α i)] :
LinearOrder (Lex ((i : ι) × α i))

The lexicographical linear order on a sigma type.

Equations
• One or more equations did not get rendered due to their size.
instance Sigma.Lex.orderBot {ι : Type u_1} {α : ιType u_2} [inst : ] [inst : ] [inst : (i : ι) → Preorder (α i)] [inst : OrderBot (α )] :
OrderBot (Lex ((i : ι) × α i))

The lexicographical linear order on a sigma type.

Equations
instance Sigma.Lex.orderTop {ι : Type u_1} {α : ιType u_2} [inst : ] [inst : ] [inst : (i : ι) → Preorder (α i)] [inst : OrderTop (α )] :
OrderTop (Lex ((i : ι) × α i))

The lexicographical linear order on a sigma type.

Equations
instance Sigma.Lex.boundedOrder {ι : Type u_1} {α : ιType u_2} [inst : ] [inst : ] [inst : (i : ι) → Preorder (α i)] [inst : OrderBot (α )] [inst : OrderTop (α )] :
BoundedOrder (Lex ((i : ι) × α i))

The lexicographical linear order on a sigma type.

Equations
• Sigma.Lex.boundedOrder = let src := Sigma.Lex.orderBot; let src_1 := Sigma.Lex.orderTop; BoundedOrder.mk
instance Sigma.Lex.denselyOrdered {ι : Type u_1} {α : ιType u_2} [inst : ] [inst : ] [inst : ∀ (i : ι), Nonempty (α i)] [inst : (i : ι) → Preorder (α i)] [inst : ∀ (i : ι), DenselyOrdered (α i)] :
DenselyOrdered (Lex ((i : ι) × α i))
Equations
instance Sigma.Lex.denselyOrdered_of_noMaxOrder {ι : Type u_1} {α : ιType u_2} [inst : ] [inst : (i : ι) → Preorder (α i)] [inst : ∀ (i : ι), DenselyOrdered (α i)] [inst : ∀ (i : ι), NoMaxOrder (α i)] :
DenselyOrdered (Lex ((i : ι) × α i))
Equations
instance Sigma.Lex.denselyOrdered_of_noMinOrder {ι : Type u_1} {α : ιType u_2} [inst : ] [inst : (i : ι) → Preorder (α i)] [inst : ∀ (i : ι), DenselyOrdered (α i)] [inst : ∀ (i : ι), NoMinOrder (α i)] :
DenselyOrdered (Lex ((i : ι) × α i))
Equations
instance Sigma.Lex.noMaxOrder_of_nonempty {ι : Type u_1} {α : ιType u_2} [inst : ] [inst : (i : ι) → Preorder (α i)] [inst : ] [inst : ∀ (i : ι), Nonempty (α i)] :
NoMaxOrder (Lex ((i : ι) × α i))
Equations
instance Sigma.Lex.noMinOrder_of_nonempty {ι : Type u_1} {α : ιType u_2} [inst : ] [inst : (i : ι) → Preorder (α i)] [inst : ] [inst : ∀ (i : ι), Nonempty (α i)] :
NoMinOrder (Lex ((i : ι) × α i))
Equations
instance Sigma.Lex.noMaxOrder {ι : Type u_1} {α : ιType u_2} [inst : ] [inst : (i : ι) → Preorder (α i)] [inst : ∀ (i : ι), NoMaxOrder (α i)] :
NoMaxOrder (Lex ((i : ι) × α i))
Equations
instance Sigma.Lex.noMinOrder {ι : Type u_1} {α : ιType u_2} [inst : ] [inst : (i : ι) → Preorder (α i)] [inst : ∀ (i : ι), NoMinOrder (α i)] :
NoMinOrder (Lex ((i : ι) × α i))
Equations