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.
• Data.Sigma.Order: Lexicographic order on Σₗ i, α i. Basically a twin of this file.
• Data.Prod.Lex: Lexicographic order on α × β× β.

TODO

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

ink

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

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

Equations

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

ink

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

• PSigma.Lex.le = { le := PSigma.Lex (fun x x_1 => x < x_1) fun x x_1 x_2 => x_1 ≤ x_2 }

ink

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

• PSigma.Lex.lt = { lt := PSigma.Lex (fun x x_1 => x < x_1) fun x x_1 x_2 => x_1 < x_2 }

ink

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

Equations

• PSigma.Lex.preorder = let src := PSigma.Lex.le; let src_1 := PSigma.Lex.lt; Preorder.mk (_ : ∀ (x : Lex ((i : ι) ×' α i)), x ≤ x) (_ : ∀ (a b c : Lex ((i : ι) ×' α i)), a ≤ b → b ≤ c → a ≤ c)

ink

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

Dictionary / lexicographic partial_order for dependent pairs.

Equations

• PSigma.Lex.partialOrder = let src := PSigma.Lex.preorder; PartialOrder.mk (_ : ∀ (a b : Lex ((i : ι) ×' α i)), a ≤ b → b ≤ a → a = b)

ink

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

Dictionary / lexicographic linear_order for pairs.

Equations

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

ink

instance PSigma.Lex.orderBot {ι : Type u_1} {α : ι → Type u_2} [inst : PartialOrder ι] [inst : OrderBot ι] [inst : (i : ι) → Preorder (α i)] [inst : OrderBot (α ⊥)] : OrderBot (Lex ((i : ι) ×' α i))

The lexicographical linear order on a sigma type.

Equations

• PSigma.Lex.orderBot = OrderBot.mk (_ : ∀ (x : Lex ((i : ι) ×' α i)), ⊥ ≤ x)

ink

instance PSigma.Lex.orderTop {ι : Type u_1} {α : ι → Type u_2} [inst : PartialOrder ι] [inst : OrderTop ι] [inst : (i : ι) → Preorder (α i)] [inst : OrderTop (α ⊤)] : OrderTop (Lex ((i : ι) ×' α i))

The lexicographical linear order on a sigma type.

Equations

• PSigma.Lex.orderTop = OrderTop.mk (_ : ∀ (x : Lex ((i : ι) ×' α i)), x ≤ ⊤)

ink

instance PSigma.Lex.boundedOrder {ι : Type u_1} {α : ι → Type u_2} [inst : PartialOrder ι] [inst : BoundedOrder ι] [inst : (i : ι) → Preorder (α i)] [inst : OrderBot (α ⊥)] [inst : OrderTop (α ⊤)] : BoundedOrder (Lex ((i : ι) ×' α i))

The lexicographical linear order on a sigma type.

Equations

• PSigma.Lex.boundedOrder = let src := PSigma.Lex.orderBot; let src_1 := PSigma.Lex.orderTop; BoundedOrder.mk

ink

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

Equations

• @PSigma.Lex.denselyOrdered = @PSigma.Lex.denselyOrdered.proof_1

ink

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

Equations

• @PSigma.Lex.denselyOrdered_of_noMaxOrder = @PSigma.Lex.denselyOrdered_of_noMaxOrder.proof_1

ink

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

Equations

• @PSigma.Lex.densely_ordered_of_noMinOrder = @PSigma.Lex.densely_ordered_of_noMinOrder.proof_1

ink

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

Equations

• @PSigma.Lex.noMaxOrder_of_nonempty = @PSigma.Lex.noMaxOrder_of_nonempty.proof_1

ink

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

Equations

• @PSigma.Lex.noMinOrder_of_nonempty = @PSigma.Lex.noMinOrder_of_nonempty.proof_1

ink

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

Equations

• @PSigma.Lex.noMaxOrder = @PSigma.Lex.noMaxOrder.proof_1

ink

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

Equations

• @PSigma.Lex.noMinOrder = @PSigma.Lex.noMinOrder.proof_1