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.

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 : ι) → LE (α i)] (_a _b : (i : ι) × α i) : Prop

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

• fiber {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → LE (α i)] (i : ι) (a b : α i) : a ≤ b → ⟨i, a⟩.LE ⟨i, b⟩

inductive Sigma.LT {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → LT (α i)] (_a _b : (i : ι) × α i) : Prop

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

• fiber {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → LT (α i)] (i : ι) (a b : α i) : a < b → ⟨i, a⟩.LT ⟨i, b⟩

instance Sigma.instLE_mathlib {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → LE (α i)] : LE ((i : ι) × α i)

Equations

• Sigma.instLE_mathlib = { le := Sigma.LE }

instance Sigma.instLT_mathlib {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → LT (α i)] : LT ((i : ι) × α i)

Equations

• Sigma.instLT_mathlib = { lt := Sigma.LT }

@[simp]

theorem Sigma.mk_le_mk_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → 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 : ι) → LT (α i)] {i : ι} {a b : α i} : ⟨i, a⟩ < ⟨i, b⟩ ↔ a < b

theorem Sigma.le_def {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → LE (α i)] {a b : (i : ι) × α i} : a ≤ b ↔ ∃ (h : a.fst = b.fst), h ▸ a.snd ≤ b.snd

theorem Sigma.lt_def {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → LT (α i)] {a b : (i : ι) × α i} : a < b ↔ ∃ (h : a.fst = b.fst), h ▸ a.snd < b.snd

instance Sigma.preorder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] : Preorder ((i : ι) × α i)

Equations

• Sigma.preorder = { toLE := Sigma.instLE_mathlib, toLT := Sigma.instLT_mathlib, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_le := ⋯ }

instance Sigma.instPartialOrder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → PartialOrder (α i)] : PartialOrder ((i : ι) × α i)

Equations

• Sigma.instPartialOrder = { toPreorder := Sigma.preorder, le_antisymm := ⋯ }

instance Sigma.instDenselyOrdered {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [∀ (i : ι), DenselyOrdered (α i)] : DenselyOrdered ((i : ι) × α i)

Lexicographical order on Sigma

def Sigma.Lex.«termΣₗ_,_» : Lean.ParserDescr

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.

def Sigma.Lex.«termΣₗ_,_».«delab_app.Lex» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

instance Sigma.Lex.LE {ι : Type u_1} {α : ι → Type u_2} [LT ι] [(i : ι) → LE (α i)] : LE (Σₗ (i : ι), α i)

The lexicographical ≤ on a sigma type.

Equations

• Sigma.Lex.LE = { le := Sigma.Lex (fun (x1 x2 : ι) => x1 < x2) fun (x : ι) (x1 x2 : α x) => x1 ≤ x2 }

instance Sigma.Lex.LT {ι : Type u_1} {α : ι → Type u_2} [LT ι] [(i : ι) → LT (α i)] : LT (Σₗ (i : ι), α i)

The lexicographical < on a sigma type.

Equations

• Sigma.Lex.LT = { lt := Sigma.Lex (fun (x1 x2 : ι) => x1 < x2) fun (x : ι) (x1 x2 : α x) => x1 < x2 }

theorem Sigma.Lex.le_def {ι : Type u_1} {α : ι → Type u_2} [LT ι] [(i : ι) → LE (α i)] {a b : Σₗ (i : ι), α i} : a ≤ b ↔ a.fst < b.fst ∨ ∃ (h : a.fst = b.fst), h ▸ a.snd ≤ b.snd

theorem Sigma.Lex.lt_def {ι : Type u_1} {α : ι → Type u_2} [LT ι] [(i : ι) → LT (α i)] {a b : Σₗ (i : ι), α i} : a < b ↔ a.fst < b.fst ∨ ∃ (h : a.fst = b.fst), h ▸ a.snd < b.snd

instance Sigma.Lex.preorder {ι : Type u_1} {α : ι → Type u_2} [Preorder ι] [(i : ι) → Preorder (α i)] : Preorder (Σₗ (i : ι), α i)

The lexicographical preorder on a sigma type.

Equations

• Sigma.Lex.preorder = { toLE := Sigma.Lex.LE, toLT := Sigma.Lex.LT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_le := ⋯ }

instance Sigma.Lex.partialOrder {ι : Type u_1} {α : ι → Type u_2} [Preorder ι] [(i : ι) → PartialOrder (α i)] : PartialOrder (Σₗ (i : ι), α i)

The lexicographical partial order on a sigma type.

Equations

• Sigma.Lex.partialOrder = { toPreorder := Sigma.Lex.preorder, le_antisymm := ⋯ }

instance Sigma.Lex.linearOrder {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : LinearOrder (Σₗ (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} [PartialOrder ι] [OrderBot ι] [(i : ι) → Preorder (α i)] [OrderBot (α ⊥)] : OrderBot (Σₗ (i : ι), α i)

The lexicographical linear order on a sigma type.

Equations

• Sigma.Lex.orderBot = { bot := ⟨⊥, ⊥⟩, bot_le := ⋯ }

instance Sigma.Lex.orderTop {ι : Type u_1} {α : ι → Type u_2} [PartialOrder ι] [OrderTop ι] [(i : ι) → Preorder (α i)] [OrderTop (α ⊤)] : OrderTop (Σₗ (i : ι), α i)

The lexicographical linear order on a sigma type.

Equations

• Sigma.Lex.orderTop = { top := ⟨⊤, ⊤⟩, le_top := ⋯ }

instance Sigma.Lex.boundedOrder {ι : Type u_1} {α : ι → Type u_2} [PartialOrder ι] [BoundedOrder ι] [(i : ι) → Preorder (α i)] [OrderBot (α ⊥)] [OrderTop (α ⊤)] : BoundedOrder (Σₗ (i : ι), α i)

The lexicographical linear order on a sigma type.

Equations

• Sigma.Lex.boundedOrder = { toOrderTop := Sigma.Lex.orderTop, toOrderBot := Sigma.Lex.orderBot }

instance Sigma.Lex.denselyOrdered {ι : Type u_1} {α : ι → Type u_2} [Preorder ι] [DenselyOrdered ι] [∀ (i : ι), Nonempty (α i)] [(i : ι) → Preorder (α i)] [∀ (i : ι), DenselyOrdered (α i)] : DenselyOrdered (Σₗ (i : ι), α i)

instance Sigma.Lex.denselyOrdered_of_noMaxOrder {ι : Type u_1} {α : ι → Type u_2} [Preorder ι] [(i : ι) → Preorder (α i)] [∀ (i : ι), DenselyOrdered (α i)] [∀ (i : ι), NoMaxOrder (α i)] : DenselyOrdered (Σₗ (i : ι), α i)

instance Sigma.Lex.denselyOrdered_of_noMinOrder {ι : Type u_1} {α : ι → Type u_2} [Preorder ι] [(i : ι) → Preorder (α i)] [∀ (i : ι), DenselyOrdered (α i)] [∀ (i : ι), NoMinOrder (α i)] : DenselyOrdered (Σₗ (i : ι), α i)

instance Sigma.Lex.noMaxOrder_of_nonempty {ι : Type u_1} {α : ι → Type u_2} [Preorder ι] [(i : ι) → Preorder (α i)] [NoMaxOrder ι] [∀ (i : ι), Nonempty (α i)] : NoMaxOrder (Σₗ (i : ι), α i)

instance Sigma.Lex.noMinOrder_of_nonempty {ι : Type u_1} {α : ι → Type u_2} [Preorder ι] [(i : ι) → Preorder (α i)] [NoMinOrder ι] [∀ (i : ι), Nonempty (α i)] : NoMinOrder (Σₗ (i : ι), α i)

instance Sigma.Lex.noMaxOrder {ι : Type u_1} {α : ι → Type u_2} [Preorder ι] [(i : ι) → Preorder (α i)] [∀ (i : ι), NoMaxOrder (α i)] : NoMaxOrder (Σₗ (i : ι), α i)

instance Sigma.Lex.noMinOrder {ι : Type u_1} {α : ι → Type u_2} [Preorder ι] [(i : ι) → Preorder (α i)] [∀ (i : ι), NoMinOrder (α i)] : NoMinOrder (Σₗ (i : ι), α i)