Documentation

Mathlib.Data.PSigma.Order

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 #

See also #

Related files are:

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.

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

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

    The lexicographical on a sigma type.

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

    The lexicographical < on a sigma type.

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

    Dictionary / lexicographic partial_order for dependent pairs.

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

    Dictionary / lexicographic linear_order for pairs.

    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.

    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.

    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.

    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.densely_ordered_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)