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 #

source
class NoBotOrder (α : Type u_3) [LE α] :
Prop

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
    source
    class NoTopOrder (α : Type u_3) [LE α] :
    Prop

    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
      source
      class NoMinOrder (α : Type u_3) [LT α] :
      Prop

      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
        source
        class NoMaxOrder (α : Type u_3) [LT α] :
        Prop

        Order without maximal elements. Sometimes called cofinal.

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

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

        Instances
          source
          instance nonempty_lt {α : Type u_1} [LT α] [NoMinOrder α] (a : α) :
          Nonempty { x : α // x < a }
          Equations
          source
          instance nonempty_gt {α : Type u_1} [LT α] [NoMaxOrder α] (a : α) :
          Nonempty { x : α // a < x }
          Equations
          source
          instance IsEmpty.toNoMaxOrder {α : Type u_1} [LT α] [IsEmpty α] :
          NoMaxOrder α
          Equations
          source
          instance IsEmpty.toNoMinOrder {α : Type u_1} [LT α] [IsEmpty α] :
          NoMinOrder α
          Equations
          source
          instance OrderDual.noBotOrder {α : Type u_1} [LE α] [NoTopOrder α] :
          NoBotOrder αᵒᵈ
          Equations
          source
          instance OrderDual.noTopOrder {α : Type u_1} [LE α] [NoBotOrder α] :
          NoTopOrder αᵒᵈ
          Equations
          source
          instance OrderDual.noMinOrder {α : Type u_1} [LT α] [NoMaxOrder α] :
          NoMinOrder αᵒᵈ
          Equations
          source
          instance OrderDual.noMaxOrder {α : Type u_1} [LT α] [NoMinOrder α] :
          NoMaxOrder αᵒᵈ
          Equations
          source
          instance instNoBotOrderToLE {α : Type u_1} [Preorder α] [NoMinOrder α] :
          NoBotOrder α
          Equations
          source
          instance instNoTopOrderToLE {α : Type u_1} [Preorder α] [NoMaxOrder α] :
          NoTopOrder α
          Equations
          source
          instance noMaxOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder α] :
          NoMaxOrder (α × β)
          Equations
          source
          instance noMaxOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder β] :
          NoMaxOrder (α × β)
          Equations
          source
          instance noMinOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder α] :
          NoMinOrder (α × β)
          Equations
          source
          instance noMinOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder β] :
          NoMinOrder (α × β)
          Equations
          source
          instance instNoMaxOrderForAllToLTPreorder {ι : Type u} {π : ι → Type u_3} [Nonempty ι] [(i : ι) → Preorder (π i)] [∀ (i : ι), NoMaxOrder (π i)] :
          NoMaxOrder ((i : ι) → π i)
          Equations
          source
          instance instNoMinOrderForAllToLTPreorder {ι : Type u} {π : ι → Type u_3} [Nonempty ι] [(i : ι) → Preorder (π i)] [∀ (i : ι), NoMinOrder (π i)] :
          NoMinOrder ((i : ι) → π i)
          Equations
          source
          theorem NoBotOrder.to_noMinOrder (α : Type u_3) [LinearOrder α] [NoBotOrder α] :
          NoMinOrder α
          source
          theorem NoTopOrder.to_noMaxOrder (α : Type u_3) [LinearOrder α] [NoTopOrder α] :
          NoMaxOrder α
          source
          theorem noBotOrder_iff_noMinOrder (α : Type u_3) [LinearOrder α] :
          NoBotOrder α ↔ NoMinOrder α
          source
          theorem noTopOrder_iff_noMaxOrder (α : Type u_3) [LinearOrder α] :
          NoTopOrder α ↔ NoMaxOrder α
          source
          theorem NoMinOrder.not_acc {α : Type u_1} [LT α] [NoMinOrder α] (a : α) :
          ¬Acc (fun (x x_1 : α) => x < x_1) a
          source
          theorem NoMaxOrder.not_acc {α : Type u_1} [LT α] [NoMaxOrder α] (a : α) :
          ¬Acc (fun (x x_1 : α) => x > x_1) a
          source
          def IsBot {α : Type u_1} [LE α] (a : α) :
          Prop

          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
            source
            def IsTop {α : Type u_1} [LE α] (a : α) :
            Prop

            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
              source
              def IsMin {α : Type u_1} [LE α] (a : α) :
              Prop

              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
                source
                def IsMax {α : Type u_1} [LE α] (a : α) :
                Prop

                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
                  source
                  @[simp]
                  theorem not_isBot {α : Type u_1} [LE α] [NoBotOrder α] (a : α) :
                  ¬IsBot a
                  source
                  @[simp]
                  theorem not_isTop {α : Type u_1} [LE α] [NoTopOrder α] (a : α) :
                  ¬IsTop a
                  source
                  theorem IsBot.isMin {α : Type u_1} [LE α] {a : α} (h : IsBot a) :
                  IsMin a
                  source
                  theorem IsTop.isMax {α : Type u_1} [LE α] {a : α} (h : IsTop a) :
                  IsMax a
                  source
                  @[simp]
                  theorem isBot_toDual_iff {α : Type u_1} [LE α] {a : α} :
                  IsBot (OrderDual.toDual a) ↔ IsTop a
                  source
                  @[simp]
                  theorem isTop_toDual_iff {α : Type u_1} [LE α] {a : α} :
                  IsTop (OrderDual.toDual a) ↔ IsBot a
                  source
                  @[simp]
                  theorem isMin_toDual_iff {α : Type u_1} [LE α] {a : α} :
                  IsMin (OrderDual.toDual a) ↔ IsMax a
                  source
                  @[simp]
                  theorem isMax_toDual_iff {α : Type u_1} [LE α] {a : α} :
                  IsMax (OrderDual.toDual a) ↔ IsMin a
                  source
                  @[simp]
                  theorem isBot_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
                  IsBot (OrderDual.ofDual a) ↔ IsTop a
                  source
                  @[simp]
                  theorem isTop_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
                  IsTop (OrderDual.ofDual a) ↔ IsBot a
                  source
                  @[simp]
                  theorem isMin_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
                  IsMin (OrderDual.ofDual a) ↔ IsMax a
                  source
                  @[simp]
                  theorem isMax_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
                  IsMax (OrderDual.ofDual a) ↔ IsMin a
                  source
                  theorem IsTop.toDual {α : Type u_1} [LE α] {a : α} :
                  IsTop a → IsBot (OrderDual.toDual a)

                  Alias of the reverse direction of isBot_toDual_iff.

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

                  Alias of the reverse direction of isTop_toDual_iff.

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

                  Alias of the reverse direction of isMin_toDual_iff.

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

                  Alias of the reverse direction of isMax_toDual_iff.

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

                  Alias of the reverse direction of isBot_ofDual_iff.

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

                  Alias of the reverse direction of isTop_ofDual_iff.

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

                  Alias of the reverse direction of isMin_ofDual_iff.

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

                  Alias of the reverse direction of isMax_ofDual_iff.

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

                  Alias of not_isMin_of_lt.

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

                  Alias of not_isMax_of_lt.

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