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_3) [LE α] :

Order without bottom elements.

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

    For each term a, there is some b which is either incomparable or strictly smaller.

Instances
    theorem NoBotOrder.exists_not_ge {α : Type u_3} [LE α] [self : NoBotOrder α] (a : α) :
    ∃ (b : α), ¬a b

    For each term a, there is some b which is either incomparable or strictly smaller.

    class NoTopOrder (α : Type u_3) [LE α] :

    Order without top elements.

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

      For each term a, there is some b which is either incomparable or strictly larger.

    Instances
      theorem NoTopOrder.exists_not_le {α : Type u_3} [LE α] [self : NoTopOrder α] (a : α) :
      ∃ (b : α), ¬b a

      For each term a, there is some b which is either incomparable or strictly larger.

      class NoMinOrder (α : Type u_3) [LT α] :

      Order without minimal elements. Sometimes called coinitial or dense.

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

        For each term a, there is some strictly smaller b.

      Instances
        theorem NoMinOrder.exists_lt {α : Type u_3} [LT α] [self : NoMinOrder α] (a : α) :
        ∃ (b : α), b < a

        For each term a, there is some strictly smaller b.

        class NoMaxOrder (α : Type u_3) [LT α] :

        Order without maximal elements. Sometimes called cofinal.

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

          For each term a, there is some strictly greater b.

        Instances
          theorem NoMaxOrder.exists_gt {α : Type u_3} [LT α] [self : NoMaxOrder α] (a : α) :
          ∃ (b : α), a < b

          For each term a, there is some strictly greater b.

          instance nonempty_lt {α : Type u_1} [LT α] [NoMinOrder α] (a : α) :
          Nonempty { x : α // x < a }
          Equations
          • =
          instance nonempty_gt {α : Type u_1} [LT α] [NoMaxOrder α] (a : α) :
          Nonempty { x : α // a < x }
          Equations
          • =
          instance IsEmpty.toNoMaxOrder {α : Type u_1} [LT α] [IsEmpty α] :
          Equations
          • =
          instance IsEmpty.toNoMinOrder {α : Type u_1} [LT α] [IsEmpty α] :
          Equations
          • =
          instance OrderDual.noBotOrder {α : Type u_1} [LE α] [NoTopOrder α] :
          Equations
          • =
          instance OrderDual.noTopOrder {α : Type u_1} [LE α] [NoBotOrder α] :
          Equations
          • =
          instance OrderDual.noMinOrder {α : Type u_1} [LT α] [NoMaxOrder α] :
          Equations
          • =
          instance OrderDual.noMaxOrder {α : Type u_1} [LT α] [NoMinOrder α] :
          Equations
          • =
          @[instance 100]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          instance noMaxOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder α] :
          NoMaxOrder (α × β)
          Equations
          • =
          instance noMaxOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder β] :
          NoMaxOrder (α × β)
          Equations
          • =
          instance noMinOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder α] :
          NoMinOrder (α × β)
          Equations
          • =
          instance noMinOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder β] :
          NoMinOrder (α × β)
          Equations
          • =
          instance instNoMaxOrderForallOfNonempty {ι : Type u} {π : ιType u_3} [Nonempty ι] [(i : ι) → Preorder (π i)] [∀ (i : ι), NoMaxOrder (π i)] :
          NoMaxOrder ((i : ι) → π i)
          Equations
          • =
          instance instNoMinOrderForallOfNonempty {ι : Type u} {π : ιType u_3} [Nonempty ι] [(i : ι) → Preorder (π i)] [∀ (i : ι), NoMinOrder (π i)] :
          NoMinOrder ((i : ι) → π i)
          Equations
          • =
          theorem NoMinOrder.not_acc {α : Type u_1} [LT α] [NoMinOrder α] (a : α) :
          ¬Acc (fun (x1 x2 : α) => x1 < x2) a
          theorem NoMaxOrder.not_acc {α : Type u_1} [LT α] [NoMaxOrder α] (a : α) :
          ¬Acc (fun (x1 x2 : α) => x1 > x2) a
          def IsBot {α : Type u_1} [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
          Instances For
            def IsTop {α : Type u_1} [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
            Instances For
              def IsMin {α : Type u_1} [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
              Instances For
                def IsMax {α : Type u_1} [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
                Instances For
                  @[simp]
                  theorem not_isBot {α : Type u_1} [LE α] [NoBotOrder α] (a : α) :
                  @[simp]
                  theorem not_isTop {α : Type u_1} [LE α] [NoTopOrder α] (a : α) :
                  theorem IsBot.isMin {α : Type u_1} [LE α] {a : α} (h : IsBot a) :
                  theorem IsTop.isMax {α : Type u_1} [LE α] {a : α} (h : IsTop a) :
                  @[simp]
                  theorem isBot_toDual_iff {α : Type u_1} [LE α] {a : α} :
                  IsBot (OrderDual.toDual a) IsTop a
                  @[simp]
                  theorem isTop_toDual_iff {α : Type u_1} [LE α] {a : α} :
                  IsTop (OrderDual.toDual a) IsBot a
                  @[simp]
                  theorem isMin_toDual_iff {α : Type u_1} [LE α] {a : α} :
                  IsMin (OrderDual.toDual a) IsMax a
                  @[simp]
                  theorem isMax_toDual_iff {α : Type u_1} [LE α] {a : α} :
                  IsMax (OrderDual.toDual a) IsMin a
                  @[simp]
                  theorem isBot_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
                  IsBot (OrderDual.ofDual a) IsTop a
                  @[simp]
                  theorem isTop_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
                  IsTop (OrderDual.ofDual a) IsBot a
                  @[simp]
                  theorem isMin_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
                  IsMin (OrderDual.ofDual a) IsMax a
                  @[simp]
                  theorem isMax_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
                  IsMax (OrderDual.ofDual a) IsMin a
                  theorem IsTop.toDual {α : Type u_1} [LE α] {a : α} :
                  IsTop aIsBot (OrderDual.toDual a)

                  Alias of the reverse direction of isBot_toDual_iff.

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

                  Alias of the reverse direction of isTop_toDual_iff.

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

                  Alias of the reverse direction of isMin_toDual_iff.

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

                  Alias of the reverse direction of isMax_toDual_iff.

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

                  Alias of the reverse direction of isBot_ofDual_iff.

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

                  Alias of the reverse direction of isTop_ofDual_iff.

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

                  Alias of the reverse direction of isMin_ofDual_iff.

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

                  Alias of the reverse direction of isMax_ofDual_iff.

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

                  Alias of not_isMin_of_lt.

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

                  Alias of not_isMax_of_lt.

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