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

• Σₗ' i, α i: Sigma type equipped with the lexicographic order. A 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.
• Order.Sigma: Lexicographic order on Σₗ i, α i. Basically a twin of this file.
• Order.Prod.Lex.Basic: Lexicographic order on α × β.

TODO

Define the disjoint order on Σ' i, α i, where x ≤ y only if x.fst = y.fst. Prove that a sigma type is a NoMaxOrder, NoMinOrder, DenselyOrdered when its summands are.

def PSigma.«termΣₗ'_,_» : Lean.ParserDescr

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

Equations

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

@[instance_reducible]

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

The lexicographical ≤ on a sigma type.

Equations

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

@[instance_reducible]

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

The lexicographical < on a sigma type.

Equations

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

@[instance_reducible]

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

Equations

• PSigma.Lex.preorder = { toLE := PSigma.Lex.le, toLT := PSigma.Lex.lt, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[instance_reducible]

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

Dictionary / lexicographic PartialOrder for dependent pairs.

Equations

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

@[instance_reducible]

instance PSigma.Lex.linearOrder {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : LinearOrder (Σₗ' (i : ι), α i)

Dictionary / lexicographic LinearOrder for pairs.

Equations

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

@[instance_reducible]

instance PSigma.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

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

@[instance_reducible]

instance PSigma.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

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

@[instance_reducible]

instance PSigma.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

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

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

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

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

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

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

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

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