Documentation

Mathlib.Order.Max

Minimal/maximal and bottom/top elements #

This file defines predicates for elements to be minimal/maximal or bottom/top and typeclasses saying that there are no such elements.

Predicates #

See also isBot_iff_isMin and isTop_iff_isMax for the equivalences in a (co)directed order.

Typeclasses #

class NoBotOrder (α : Type u_1) [inst : LE α] :
  • For each term a, there is some b which is either incomparable or strictly smaller.

    exists_not_ge : ∀ (a : α), b, ¬a b

Order without bottom elements.

Instances
    class NoTopOrder (α : Type u_1) [inst : LE α] :
    • For each term a, there is some b which is either incomparable or strictly larger.

      exists_not_le : ∀ (a : α), b, ¬b a

    Order without top elements.

    Instances
      class NoMinOrder (α : Type u_1) [inst : LT α] :
      • For each term a, there is some strictly smaller b.

        exists_lt : ∀ (a : α), b, b < a

      Order without minimal elements. Sometimes called coinitial or dense.

      Instances
        class NoMaxOrder (α : Type u_1) [inst : LT α] :
        • For each term a, there is some strictly greater b.

          exists_gt : ∀ (a : α), b, a < b

        Order without maximal elements. Sometimes called cofinal.

        Instances
          instance nonempty_lt {α : Type u_1} [inst : LT α] [inst : NoMinOrder α] (a : α) :
          Nonempty { x // x < a }
          Equations
          instance nonempty_gt {α : Type u_1} [inst : LT α] [inst : NoMaxOrder α] (a : α) :
          Nonempty { x // a < x }
          Equations
          instance noMaxOrder_of_left {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : NoMaxOrder α] :
          NoMaxOrder (α × β)
          Equations
          instance noMaxOrder_of_right {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : NoMaxOrder β] :
          NoMaxOrder (α × β)
          Equations
          instance noMinOrder_of_left {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : NoMinOrder α] :
          NoMinOrder (α × β)
          Equations
          instance noMinOrder_of_right {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : NoMinOrder β] :
          NoMinOrder (α × β)
          Equations
          instance instNoMaxOrderForAllToLTPreorder {ι : Type u} {π : ιType u_1} [inst : Nonempty ι] [inst : (i : ι) → Preorder (π i)] [inst : ∀ (i : ι), NoMaxOrder (π i)] :
          NoMaxOrder ((i : ι) → π i)
          Equations
          instance instNoMinOrderForAllToLTPreorder {ι : Type u} {π : ιType u_1} [inst : Nonempty ι] [inst : (i : ι) → Preorder (π i)] [inst : ∀ (i : ι), NoMinOrder (π i)] :
          NoMinOrder ((i : ι) → π i)
          Equations
          theorem NoBotOrder.to_noMinOrder (α : Type u_1) [inst : LinearOrder α] [inst : NoBotOrder α] :
          theorem NoTopOrder.to_noMaxOrder (α : Type u_1) [inst : LinearOrder α] [inst : NoTopOrder α] :
          theorem NoMinOrder.not_acc {α : Type u_1} [inst : LT α] [inst : NoMinOrder α] (a : α) :
          ¬Acc (fun x x_1 => x < x_1) a
          theorem NoMaxOrder.not_acc {α : Type u_1} [inst : LT α] [inst : NoMaxOrder α] (a : α) :
          ¬Acc (fun x x_1 => x > x_1) a
          def IsBot {α : Type u_1} [inst : LE α] (a : α) :

          a : α is a bottom element of α if it is less than or equal to any other element of α. This predicate is roughly an unbundled version of OrderBot, except that a preorder may have several bottom elements. When α is linear, this is useful to make a case disjunction on NoMinOrder α within a proof.

          Equations
          def IsTop {α : Type u_1} [inst : LE α] (a : α) :

          a : α is a top element of α if it is greater than or equal to any other element of α. This predicate is roughly an unbundled version of OrderBot, except that a preorder may have several top elements. When α is linear, this is useful to make a case disjunction on NoMaxOrder α within a proof.

          Equations
          def IsMin {α : Type u_1} [inst : LE α] (a : α) :

          a is a minimal element of α if no element is strictly less than it. We spell it without < to avoid having to convert between ≤≤ and <. Instead, isMin_iff_forall_not_lt does the conversion.

          Equations
          def IsMax {α : Type u_1} [inst : LE α] (a : α) :

          a is a maximal element of α if no element is strictly greater than it. We spell it without < to avoid having to convert between ≤≤ and <. Instead, isMax_iff_forall_not_lt does the conversion.

          Equations
          @[simp]
          theorem not_isBot {α : Type u_1} [inst : LE α] [inst : NoBotOrder α] (a : α) :
          @[simp]
          theorem not_isTop {α : Type u_1} [inst : LE α] [inst : NoTopOrder α] (a : α) :
          theorem IsBot.isMin {α : Type u_1} [inst : LE α] {a : α} (h : IsBot a) :
          theorem IsTop.isMax {α : Type u_1} [inst : LE α] {a : α} (h : IsTop a) :
          @[simp]
          theorem isBot_toDual_iff {α : Type u_1} [inst : LE α] {a : α} :
          IsBot (OrderDual.toDual a) IsTop a
          @[simp]
          theorem isTop_toDual_iff {α : Type u_1} [inst : LE α] {a : α} :
          IsTop (OrderDual.toDual a) IsBot a
          @[simp]
          theorem isMin_toDual_iff {α : Type u_1} [inst : LE α] {a : α} :
          IsMin (OrderDual.toDual a) IsMax a
          @[simp]
          theorem isMax_toDual_iff {α : Type u_1} [inst : LE α] {a : α} :
          IsMax (OrderDual.toDual a) IsMin a
          @[simp]
          theorem isBot_ofDual_iff {α : Type u_1} [inst : LE α] {a : αᵒᵈ} :
          IsBot (OrderDual.ofDual a) IsTop a
          @[simp]
          theorem isTop_ofDual_iff {α : Type u_1} [inst : LE α] {a : αᵒᵈ} :
          IsTop (OrderDual.ofDual a) IsBot a
          @[simp]
          theorem isMin_ofDual_iff {α : Type u_1} [inst : LE α] {a : αᵒᵈ} :
          IsMin (OrderDual.ofDual a) IsMax a
          @[simp]
          theorem isMax_ofDual_iff {α : Type u_1} [inst : LE α] {a : αᵒᵈ} :
          IsMax (OrderDual.ofDual a) IsMin a
          theorem IsTop.toDual {α : Type u_1} [inst : LE α] {a : α} :
          IsTop aIsBot (OrderDual.toDual a)

          Alias of the reverse direction of isBot_toDual_iff.

          theorem IsBot.toDual {α : Type u_1} [inst : LE α] {a : α} :
          IsBot aIsTop (OrderDual.toDual a)

          Alias of the reverse direction of isTop_toDual_iff.

          theorem IsMax.toDual {α : Type u_1} [inst : LE α] {a : α} :
          IsMax aIsMin (OrderDual.toDual a)

          Alias of the reverse direction of isMin_toDual_iff.

          theorem IsMin.toDual {α : Type u_1} [inst : LE α] {a : α} :
          IsMin aIsMax (OrderDual.toDual a)

          Alias of the reverse direction of isMax_toDual_iff.

          theorem IsTop.ofDual {α : Type u_1} [inst : LE α] {a : αᵒᵈ} :
          IsTop aIsBot (OrderDual.ofDual a)

          Alias of the reverse direction of isBot_ofDual_iff.

          theorem IsBot.ofDual {α : Type u_1} [inst : LE α] {a : αᵒᵈ} :
          IsBot aIsTop (OrderDual.ofDual a)

          Alias of the reverse direction of isTop_ofDual_iff.

          theorem IsMax.ofDual {α : Type u_1} [inst : LE α] {a : αᵒᵈ} :
          IsMax aIsMin (OrderDual.ofDual a)

          Alias of the reverse direction of isMin_ofDual_iff.

          theorem IsMin.ofDual {α : Type u_1} [inst : LE α] {a : αᵒᵈ} :
          IsMin aIsMax (OrderDual.ofDual a)

          Alias of the reverse direction of isMax_ofDual_iff.

          theorem IsBot.mono {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (ha : IsBot a) (h : b a) :
          theorem IsTop.mono {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (ha : IsTop a) (h : a b) :
          theorem IsMin.mono {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (ha : IsMin a) (h : b a) :
          theorem IsMax.mono {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (ha : IsMax a) (h : a b) :
          theorem IsMin.not_lt {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (h : IsMin a) :
          ¬b < a
          theorem IsMax.not_lt {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (h : IsMax a) :
          ¬a < b
          @[simp]
          theorem not_isMin_of_lt {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (h : b < a) :
          @[simp]
          theorem not_isMax_of_lt {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (h : a < b) :
          theorem LT.lt.not_isMin {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (h : b < a) :

          Alias of not_isMin_of_lt.

          theorem LT.lt.not_isMax {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (h : a < b) :

          Alias of not_isMax_of_lt.

          theorem isMin_iff_forall_not_lt {α : Type u_1} [inst : Preorder α] {a : α} :
          IsMin a ∀ (b : α), ¬b < a
          theorem isMax_iff_forall_not_lt {α : Type u_1} [inst : Preorder α] {a : α} :
          IsMax a ∀ (b : α), ¬a < b
          @[simp]
          theorem not_isMin_iff {α : Type u_1} [inst : Preorder α] {a : α} :
          ¬IsMin a b, b < a
          @[simp]
          theorem not_isMax_iff {α : Type u_1} [inst : Preorder α] {a : α} :
          ¬IsMax a b, a < b
          @[simp]
          theorem not_isMin {α : Type u_1} [inst : Preorder α] [inst : NoMinOrder α] (a : α) :
          @[simp]
          theorem not_isMax {α : Type u_1} [inst : Preorder α] [inst : NoMaxOrder α] (a : α) :
          theorem Subsingleton.isBot {α : Type u_1} [inst : Preorder α] [inst : Subsingleton α] (a : α) :
          theorem Subsingleton.isTop {α : Type u_1} [inst : Preorder α] [inst : Subsingleton α] (a : α) :
          theorem Subsingleton.isMin {α : Type u_1} [inst : Preorder α] [inst : Subsingleton α] (a : α) :
          theorem Subsingleton.isMax {α : Type u_1} [inst : Preorder α] [inst : Subsingleton α] (a : α) :
          theorem IsMin.eq_of_le {α : Type u_1} [inst : PartialOrder α] {a : α} {b : α} (ha : IsMin a) (h : b a) :
          b = a
          theorem IsMin.eq_of_ge {α : Type u_1} [inst : PartialOrder α] {a : α} {b : α} (ha : IsMin a) (h : b a) :
          a = b
          theorem IsMax.eq_of_le {α : Type u_1} [inst : PartialOrder α] {a : α} {b : α} (ha : IsMax a) (h : a b) :
          a = b
          theorem IsMax.eq_of_ge {α : Type u_1} [inst : PartialOrder α] {a : α} {b : α} (ha : IsMax a) (h : a b) :
          b = a
          theorem IsBot.prod_mk {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {a : α} {b : β} (ha : IsBot a) (hb : IsBot b) :
          IsBot (a, b)
          theorem IsTop.prod_mk {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {a : α} {b : β} (ha : IsTop a) (hb : IsTop b) :
          IsTop (a, b)
          theorem IsMin.prod_mk {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {a : α} {b : β} (ha : IsMin a) (hb : IsMin b) :
          IsMin (a, b)
          theorem IsMax.prod_mk {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {a : α} {b : β} (ha : IsMax a) (hb : IsMax b) :
          IsMax (a, b)
          theorem IsBot.fst {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {x : α × β} (hx : IsBot x) :
          IsBot x.fst
          theorem IsBot.snd {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {x : α × β} (hx : IsBot x) :
          IsBot x.snd
          theorem IsTop.fst {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {x : α × β} (hx : IsTop x) :
          IsTop x.fst
          theorem IsTop.snd {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {x : α × β} (hx : IsTop x) :
          IsTop x.snd
          theorem IsMin.fst {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {x : α × β} (hx : IsMin x) :
          IsMin x.fst
          theorem IsMin.snd {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {x : α × β} (hx : IsMin x) :
          IsMin x.snd
          theorem IsMax.fst {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {x : α × β} (hx : IsMax x) :
          IsMax x.fst
          theorem IsMax.snd {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {x : α × β} (hx : IsMax x) :
          IsMax x.snd
          theorem Prod.isBot_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {x : α × β} :
          IsBot x IsBot x.fst IsBot x.snd
          theorem Prod.isTop_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {x : α × β} :
          IsTop x IsTop x.fst IsTop x.snd
          theorem Prod.isMin_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {x : α × β} :
          IsMin x IsMin x.fst IsMin x.snd
          theorem Prod.isMax_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {x : α × β} :
          IsMax x IsMax x.fst IsMax x.snd