Documentation

Mathlib.Data.Pi.Lex

Lexicographic order on Pi types #

This file defines the lexicographic order for Pi types. a is less than b if a i = b i for all i up to some point k, and a k < b k.

Notation #

See also #

Related files are:

def Pi.Lex {ι : Type u_1} {β : ιType u_2} (r : ιιProp) (s : {i : ι} → β iβ iProp) (x : (i : ι) → β i) (y : (i : ι) → β i) :

The lexicographic relation on Π i : ι, β i, where ι is ordered by r, and each β i is ordered by s.

Equations
  • Pi.Lex r s x y = i, (∀ (j : ι), r j ix j = y j) s i (x i) (y i)
Instances For

    The notation Πₗ i, α i refers to a pi type equipped with the lexicographic order.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Pi.toLex_apply {ι : Type u_1} {β : ιType u_2} (x : (i : ι) → β i) (i : ι) :
      toLex x i = x i
      @[simp]
      theorem Pi.ofLex_apply {ι : Type u_1} {β : ιType u_2} (x : Lex ((i : ι) → β i)) (i : ι) :
      ofLex x i = x i
      theorem Pi.lex_lt_of_lt_of_preorder {ι : Type u_1} {β : ιType u_2} [(i : ι) → Preorder (β i)] {r : ιιProp} (hwf : WellFounded r) {x : (i : ι) → β i} {y : (i : ι) → β i} (hlt : x < y) :
      i, (∀ (j : ι), r j ix j y j y j x j) x i < y i
      theorem Pi.lex_lt_of_lt {ι : Type u_1} {β : ιType u_2} [(i : ι) → PartialOrder (β i)] {r : ιιProp} (hwf : WellFounded r) {x : (i : ι) → β i} {y : (i : ι) → β i} (hlt : x < y) :
      Pi.Lex r (fun i x x_1 => x < x_1) x y
      theorem Pi.isTrichotomous_lex {ι : Type u_1} {β : ιType u_2} (r : ιιProp) (s : {i : ι} → β iβ iProp) [∀ (i : ι), IsTrichotomous (β i) (s i)] (wf : WellFounded r) :
      IsTrichotomous ((i : ι) → β i) (Pi.Lex r s)
      instance Pi.instLTLexForAll {ι : Type u_1} {β : ιType u_2} [LT ι] [(a : ι) → LT (β a)] :
      LT (Lex ((i : ι) → β i))
      Equations
      • Pi.instLTLexForAll = { lt := Pi.Lex (fun x x_1 => x < x_1) fun x x_1 x_2 => x_1 < x_2 }
      instance Pi.Lex.isStrictOrder {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [(a : ι) → PartialOrder (β a)] :
      IsStrictOrder (Lex ((i : ι) → β i)) fun x x_1 => x < x_1
      Equations
      instance Pi.instPartialOrderLexForAll {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [(a : ι) → PartialOrder (β a)] :
      PartialOrder (Lex ((i : ι) → β i))
      Equations
      noncomputable instance Pi.instLinearOrderLexForAll {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(a : ι) → LinearOrder (β a)] :
      LinearOrder (Lex ((i : ι) → β i))

      Πₗ i, α i is a linear order if the original order is well-founded.

      Equations
      theorem Pi.toLex_monotone {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → PartialOrder (β i)] :
      Monotone toLex
      theorem Pi.toLex_strictMono {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → PartialOrder (β i)] :
      StrictMono toLex
      @[simp]
      theorem Pi.lt_toLex_update_self_iff {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} :
      toLex x < toLex (Function.update x i a) x i < a
      @[simp]
      theorem Pi.toLex_update_lt_self_iff {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} :
      toLex (Function.update x i a) < toLex x a < x i
      @[simp]
      theorem Pi.le_toLex_update_self_iff {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} :
      toLex x toLex (Function.update x i a) x i a
      @[simp]
      theorem Pi.toLex_update_le_self_iff {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} :
      toLex (Function.update x i a) toLex x a x i
      instance Pi.instOrderBotLexForAllToLEToPreorderInstPartialOrderLexForAll {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(a : ι) → PartialOrder (β a)] [(a : ι) → OrderBot (β a)] :
      OrderBot (Lex ((a : ι) → β a))
      Equations
      • Pi.instOrderBotLexForAllToLEToPreorderInstPartialOrderLexForAll = OrderBot.mk (_ : ∀ (x : Lex ((a : ι) → β a)), toLex toLex x)
      instance Pi.instOrderTopLexForAllToLEToPreorderInstPartialOrderLexForAll {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(a : ι) → PartialOrder (β a)] [(a : ι) → OrderTop (β a)] :
      OrderTop (Lex ((a : ι) → β a))
      Equations
      • Pi.instOrderTopLexForAllToLEToPreorderInstPartialOrderLexForAll = OrderTop.mk (_ : ∀ (x : Lex ((a : ι) → β a)), toLex x toLex )
      instance Pi.instBoundedOrderLexForAllToLEToPreorderInstPartialOrderLexForAll {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(a : ι) → PartialOrder (β a)] [(a : ι) → BoundedOrder (β a)] :
      BoundedOrder (Lex ((a : ι) → β a))
      Equations
      • Pi.instBoundedOrderLexForAllToLEToPreorderInstPartialOrderLexForAll = BoundedOrder.mk
      theorem Pi.Lex.noMaxOrder' {ι : Type u_1} {β : ιType u_2} [Preorder ι] [(i : ι) → LT (β i)] (i : ι) [NoMaxOrder (β i)] :
      NoMaxOrder (Lex ((i : ι) → β i))
      instance Pi.instNoMaxOrderLexForAllInstLTLexForAllToLTToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeToLTToPreorder {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [Nonempty ι] [(i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMaxOrder (β i)] :
      NoMaxOrder (Lex ((i : ι) → β i))
      Equations
      • One or more equations did not get rendered due to their size.
      instance Pi.instNoMinOrderLexForAllInstLTLexForAllToLTToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeToLTToPreorder {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [Nonempty ι] [(i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMinOrder (β i)] :
      NoMinOrder (Lex ((i : ι) → β i))
      Equations
      • One or more equations did not get rendered due to their size.
      instance Pi.Lex.orderedAddCancelCommMonoid {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (β i)] :
      OrderedCancelAddCommMonoid (Lex ((i : ι) → β i))
      Equations
      • One or more equations did not get rendered due to their size.
      abbrev Pi.Lex.orderedAddCancelCommMonoid.match_1 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (β i)] :
      (x x_1 : Lex ((i : ι) → β i)) → (motive : x < x_1Prop) → ∀ (x_2 : x < x_1), (∀ (i : ι) (hi : (∀ (j : ι), j < ix j = x_1 j) (fun x x_3 x_4 => x_3 < x_4) i (x i) (x_1 i)), motive (_ : i, (∀ (j : ι), j < ix j = x_1 j) (fun x x_3 x_4 => x_3 < x_4) i (x i) (x_1 i))) → motive x_2
      Equations
      Instances For
        theorem Pi.Lex.orderedAddCancelCommMonoid.proof_2 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (β i)] :
        ∀ (x x_1 x_2 : Lex ((i : ι) → β i)), x + x_1 x + x_2x_1 x_2
        abbrev Pi.Lex.orderedAddCancelCommMonoid.match_2 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (β i)] :
        (x x_1 x_2 : Lex ((i : ι) → β i)) → (motive : x + x_1 < x + x_2Prop) → ∀ (x_3 : x + x_1 < x + x_2), (∀ (i : ι) (hi : (∀ (j : ι), j < i(Lex ((i : ι) → β i) + Lex ((i : ι) → β i)) (Lex ((i : ι) → β i)) instHAdd x x_1 j = (Lex ((i : ι) → β i) + Lex ((i : ι) → β i)) (Lex ((i : ι) → β i)) instHAdd x x_2 j) (fun x x_4 x_5 => x_4 < x_5) i ((Lex ((i : ι) → β i) + Lex ((i : ι) → β i)) (Lex ((i : ι) → β i)) instHAdd x x_1 i) ((Lex ((i : ι) → β i) + Lex ((i : ι) → β i)) (Lex ((i : ι) → β i)) instHAdd x x_2 i)), motive (_ : i, (∀ (j : ι), j < i(Lex ((i : ι) → β i) + Lex ((i : ι) → β i)) (Lex ((i : ι) → β i)) instHAdd x x_1 j = (Lex ((i : ι) → β i) + Lex ((i : ι) → β i)) (Lex ((i : ι) → β i)) instHAdd x x_2 j) (fun x x_4 x_5 => x_4 < x_5) i ((Lex ((i : ι) → β i) + Lex ((i : ι) → β i)) (Lex ((i : ι) → β i)) instHAdd x x_1 i) ((Lex ((i : ι) → β i) + Lex ((i : ι) → β i)) (Lex ((i : ι) → β i)) instHAdd x x_2 i))) → motive x_3
        Equations
        Instances For
          theorem Pi.Lex.orderedAddCancelCommMonoid.proof_1 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (β i)] :
          ∀ (x x_1 : Lex ((i : ι) → β i)), x x_1∀ (z : Lex ((i : ι) → β i)), z + x z + x_1
          instance Pi.Lex.orderedCancelCommMonoid {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedCancelCommMonoid (β i)] :
          OrderedCancelCommMonoid (Lex ((i : ι) → β i))
          Equations
          • One or more equations did not get rendered due to their size.
          theorem Pi.Lex.orderedAddCommGroup.proof_1 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedAddCommGroup (β i)] :
          ∀ (x x_1 : Lex ((i : ι) → β i)), x x_1∀ (a : Lex ((i : ι) → β i)), a + x a + x_1
          instance Pi.Lex.orderedAddCommGroup {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedAddCommGroup (β i)] :
          OrderedAddCommGroup (Lex ((i : ι) → β i))
          Equations
          instance Pi.Lex.orderedCommGroup {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedCommGroup (β i)] :
          OrderedCommGroup (Lex ((i : ι) → β i))
          Equations
          theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_5 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → LinearOrderedCancelAddCommMonoid (β i)] (a : Lex ((i : ι) → β i)) (b : Lex ((i : ι) → β i)) :
          max a b = if a b then b else a
          theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_4 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → LinearOrderedCancelAddCommMonoid (β i)] (a : Lex ((i : ι) → β i)) (b : Lex ((i : ι) → β i)) :
          min a b = if a b then a else b
          theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_6 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → LinearOrderedCancelAddCommMonoid (β i)] (a : Lex ((i : ι) → β i)) (b : Lex ((i : ι) → β i)) :
          theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_2 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [(i : ι) → LinearOrderedCancelAddCommMonoid (β i)] (a : Lex ((i : ι) → β i)) (b : Lex ((i : ι) → β i)) (c : Lex ((i : ι) → β i)) :
          a + b a + cb c
          theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_1 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [(i : ι) → LinearOrderedCancelAddCommMonoid (β i)] (a : Lex ((i : ι) → β i)) (b : Lex ((i : ι) → β i)) :
          a b∀ (c : Lex ((i : ι) → β i)), c + a c + b
          theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_3 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → LinearOrderedCancelAddCommMonoid (β i)] (a : Lex ((i : ι) → β i)) (b : Lex ((i : ι) → β i)) :
          a b b a
          noncomputable instance Pi.Lex.linearOrderedAddCancelCommMonoid {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → LinearOrderedCancelAddCommMonoid (β i)] :
          Equations
          • One or more equations did not get rendered due to their size.
          noncomputable instance Pi.Lex.linearOrderedCancelCommMonoid {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → LinearOrderedCancelCommMonoid (β i)] :
          LinearOrderedCancelCommMonoid (Lex ((i : ι) → β i))
          Equations
          • One or more equations did not get rendered due to their size.
          theorem Pi.Lex.linearOrderedAddCommGroup.proof_1 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → LinearOrderedAddCommGroup (β i)] :
          ∀ (x x_1 : Lex ((i : ι) → β i)), x x_1∀ (a : Lex ((i : ι) → β i)), a + x a + x_1
          theorem Pi.Lex.linearOrderedAddCommGroup.proof_3 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → LinearOrderedAddCommGroup (β i)] (a : Lex ((i : ι) → β i)) (b : Lex ((i : ι) → β i)) :
          min a b = if a b then a else b
          theorem Pi.Lex.linearOrderedAddCommGroup.proof_4 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → LinearOrderedAddCommGroup (β i)] (a : Lex ((i : ι) → β i)) (b : Lex ((i : ι) → β i)) :
          max a b = if a b then b else a
          noncomputable instance Pi.Lex.linearOrderedAddCommGroup {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → LinearOrderedAddCommGroup (β i)] :
          LinearOrderedAddCommGroup (Lex ((i : ι) → β i))
          Equations
          • One or more equations did not get rendered due to their size.
          theorem Pi.Lex.linearOrderedAddCommGroup.proof_5 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → LinearOrderedAddCommGroup (β i)] (a : Lex ((i : ι) → β i)) (b : Lex ((i : ι) → β i)) :
          theorem Pi.Lex.linearOrderedAddCommGroup.proof_2 {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → LinearOrderedAddCommGroup (β i)] (a : Lex ((i : ι) → β i)) (b : Lex ((i : ι) → β i)) :
          a b b a
          noncomputable instance Pi.Lex.linearOrderedCommGroup {ι : Type u_1} {β : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun x x_1 => x < x_1] [(i : ι) → LinearOrderedCommGroup (β i)] :
          LinearOrderedCommGroup (Lex ((i : ι) → β i))
          Equations
          • One or more equations did not get rendered due to their size.
          theorem Pi.lex_desc {ι : Type u_1} {α : Type u_3} [Preorder ι] [DecidableEq ι] [Preorder α] {f : ια} {i : ι} {j : ι} (h₁ : i j) (h₂ : f j < f i) :
          toLex (f ↑(Equiv.swap i j)) < toLex f

          If we swap two strictly decreasing values in a function, then the result is lexicographically smaller than the original function.