Documentation

Mathlib.Data.Sigma.Order

Orders on a sigma type #

This file defines two orders on a sigma type:

We make the disjoint sum of orders the default set of instances. The lexicographic order goes on a type synonym.

Notation #

See also #

Related files are:

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 : (i : ι) × α i) (_b : (i : ι) × α i) :

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

  • fiber: ∀ {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → LE (α i)] (i : ι) (a b : α i), a bi, a.le i, b
Instances For
    inductive Sigma.lt {ι : Type u_1} {α : ιType u_2} [(i : ι) → LT (α i)] (_a : (i : ι) × α i) (_b : (i : ι) × α i) :

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

    • fiber: ∀ {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → LT (α i)] (i : ι) (a b : α i), a < bi, a.lt i, b
    Instances For
      instance Sigma.LE {ι : Type u_1} {α : ιType u_2} [(i : ι) → LE (α i)] :
      LE ((i : ι) × α i)
      Equations
      • Sigma.LE = { le := Sigma.le }
      instance Sigma.LT {ι : Type u_1} {α : ιType u_2} [(i : ι) → LT (α i)] :
      LT ((i : ι) × α i)
      Equations
      • Sigma.LT = { lt := Sigma.lt }
      @[simp]
      theorem Sigma.mk_le_mk_iff {ι : Type u_1} {α : ιType u_2} [(i : ι) → LE (α i)] {i : ι} {a : α i} {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 : α i} {b : α i} :
      i, a < i, b a < b
      theorem Sigma.le_def {ι : Type u_1} {α : ιType u_2} [(i : ι) → LE (α i)] {a : (i : ι) × α i} {b : (i : ι) × α i} :
      a b ∃ (h : a.fst = b.fst), ha.snd b.snd
      theorem Sigma.lt_def {ι : Type u_1} {α : ιType u_2} [(i : ι) → LT (α i)] {a : (i : ι) × α i} {b : (i : ι) × α i} :
      a < b ∃ (h : a.fst = b.fst), ha.snd < b.snd
      instance Sigma.preorder {ι : Type u_1} {α : ιType u_2} [(i : ι) → Preorder (α i)] :
      Preorder ((i : ι) × α i)
      Equations
      • Sigma.preorder = let __src := Sigma.LE; let __src_1 := Sigma.LT; Preorder.mk
      instance Sigma.instPartialOrder {ι : Type u_1} {α : ιType u_2} [(i : ι) → PartialOrder (α i)] :
      PartialOrder ((i : ι) × α i)
      Equations
      instance Sigma.instDenselyOrdered {ι : Type u_1} {α : ιType u_2} [(i : ι) → Preorder (α i)] [∀ (i : ι), DenselyOrdered (α i)] :
      DenselyOrdered ((i : ι) × α i)
      Equations
      • =

      Lexicographical order on Sigma #

      Pretty printer defined by notation3 command.

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

        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.
        Instances For
          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 (x x_1 : ι) => x < x_1) fun (x : ι) (x_1 x_2 : α x) => x_1 x_2 }
          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 (x x_1 : ι) => x < x_1) fun (x : ι) (x_1 x_2 : α x) => x_1 < x_2 }
          theorem Sigma.Lex.le_def {ι : Type u_1} {α : ιType u_2} [LT ι] [(i : ι) → LE (α i)] {a : Σₗ (i : ι), α i} {b : Σₗ (i : ι), α i} :
          a b a.fst < b.fst ∃ (h : a.fst = b.fst), ha.snd b.snd
          theorem Sigma.Lex.lt_def {ι : Type u_1} {α : ιType u_2} [LT ι] [(i : ι) → LT (α i)] {a : Σₗ (i : ι), α i} {b : Σₗ (i : ι), α i} :
          a < b a.fst < b.fst ∃ (h : a.fst = b.fst), ha.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 = let __src := Sigma.Lex.LE; let __src_1 := Sigma.Lex.LT; Preorder.mk
          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
          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
          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
          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 = let __src := Sigma.Lex.orderBot; let __src_1 := Sigma.Lex.orderTop; BoundedOrder.mk
          instance Sigma.Lex.denselyOrdered {ι : Type u_1} {α : ιType u_2} [Preorder ι] [DenselyOrdered ι] [∀ (i : ι), Nonempty (α i)] [(i : ι) → Preorder (α i)] [∀ (i : ι), DenselyOrdered (α i)] :
          DenselyOrdered (Σₗ (i : ι), α i)
          Equations
          • =
          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)
          Equations
          • =
          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)
          Equations
          • =
          instance Sigma.Lex.noMaxOrder_of_nonempty {ι : Type u_1} {α : ιType u_2} [Preorder ι] [(i : ι) → Preorder (α i)] [NoMaxOrder ι] [∀ (i : ι), Nonempty (α i)] :
          NoMaxOrder (Σₗ (i : ι), α i)
          Equations
          • =
          instance Sigma.Lex.noMinOrder_of_nonempty {ι : Type u_1} {α : ιType u_2} [Preorder ι] [(i : ι) → Preorder (α i)] [NoMinOrder ι] [∀ (i : ι), Nonempty (α i)] :
          NoMinOrder (Σₗ (i : ι), α i)
          Equations
          • =
          instance Sigma.Lex.noMaxOrder {ι : Type u_1} {α : ιType u_2} [Preorder ι] [(i : ι) → Preorder (α i)] [∀ (i : ι), NoMaxOrder (α i)] :
          NoMaxOrder (Σₗ (i : ι), α i)
          Equations
          • =
          instance Sigma.Lex.noMinOrder {ι : Type u_1} {α : ιType u_2} [Preorder ι] [(i : ι) → Preorder (α i)] [∀ (i : ι), NoMinOrder (α i)] :
          NoMinOrder (Σₗ (i : ι), α i)
          Equations
          • =