Documentation

Mathlib.Order.BoundedOrder

⊤ and ⊥, bounded lattices and variants #

This file defines top and bottom elements (greatest and least elements) of a type, the bounded variants of different kinds of lattices, sets up the typeclass hierarchy between them and provides instances for Prop and fun.

Main declarations #

Common lattices #

Top, bottom element #

class OrderTop (α : Type u) [LE α] extends Top :

An order is an OrderTop if it has a greatest element. We state this using a data mixin, holding the value of and the greatest element constraint.

  • top : α
  • le_top : ∀ (a : α), a

    is the greatest element

Instances
    theorem OrderTop.le_top {α : Type u} :
    ∀ {inst : LE α} [self : OrderTop α] (a : α), a

    is the greatest element

    noncomputable def topOrderOrNoTopOrder (α : Type u_3) [LE α] :

    An order is (noncomputably) either an OrderTop or a NoTopOrder. Use as casesI topOrderOrNoTopOrder α.

    Equations
    Instances For
      @[simp]
      theorem le_top {α : Type u} [LE α] [OrderTop α] {a : α} :
      @[simp]
      theorem isTop_top {α : Type u} [LE α] [OrderTop α] :
      @[simp]
      theorem isMax_top {α : Type u} [Preorder α] [OrderTop α] :
      @[simp]
      theorem not_top_lt {α : Type u} [Preorder α] [OrderTop α] {a : α} :
      theorem ne_top_of_lt {α : Type u} [Preorder α] [OrderTop α] {a : α} {b : α} (h : a < b) :
      theorem LT.lt.ne_top {α : Type u} [Preorder α] [OrderTop α] {a : α} {b : α} (h : a < b) :

      Alias of ne_top_of_lt.

      theorem lt_top_of_lt {α : Type u} [Preorder α] [OrderTop α] {a : α} {b : α} (h : a < b) :
      a <
      theorem LT.lt.lt_top {α : Type u} [Preorder α] [OrderTop α] {a : α} {b : α} (h : a < b) :
      a <

      Alias of lt_top_of_lt.

      @[simp]
      theorem isMax_iff_eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
      @[simp]
      theorem isTop_iff_eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
      theorem not_isMax_iff_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
      theorem not_isTop_iff_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
      theorem IsMax.eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
      IsMax aa =

      Alias of the forward direction of isMax_iff_eq_top.

      theorem IsTop.eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
      IsTop aa =

      Alias of the forward direction of isTop_iff_eq_top.

      @[simp]
      theorem top_le_iff {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
      theorem top_unique {α : Type u} [PartialOrder α] [OrderTop α] {a : α} (h : a) :
      a =
      theorem eq_top_iff {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
      theorem eq_top_mono {α : Type u} [PartialOrder α] [OrderTop α] {a : α} {b : α} (h : a b) (h₂ : a = ) :
      b =
      theorem lt_top_iff_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
      @[simp]
      theorem not_lt_top_iff {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
      theorem eq_top_or_lt_top {α : Type u} [PartialOrder α] [OrderTop α] (a : α) :
      a = a <
      theorem Ne.lt_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} (h : a ) :
      a <
      theorem Ne.lt_top' {α : Type u} [PartialOrder α] [OrderTop α] {a : α} (h : a) :
      a <
      theorem ne_top_of_le_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} {b : α} (hb : b ) (hab : a b) :
      theorem StrictMono.apply_eq_top_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderTop α] [Preorder β] {f : αβ} {a : α} (hf : StrictMono f) :
      f a = f a =
      theorem StrictAnti.apply_eq_top_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderTop α] [Preorder β] {f : αβ} {a : α} (hf : StrictAnti f) :
      f a = f a =
      theorem top_not_mem_iff {α : Type u} [PartialOrder α] [OrderTop α] {s : Set α} :
      ¬ s ∀ (x : α), x sx <
      theorem StrictMono.maximal_preimage_top {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] [OrderTop β] {f : αβ} (H : StrictMono f) {a : α} (h_top : f a = ) (x : α) :
      x a
      theorem OrderTop.ext_top {α : Type u_3} {hA : PartialOrder α} (A : OrderTop α) {hB : PartialOrder α} (B : OrderTop α) (H : ∀ (x y : α), x y x y) :
      class OrderBot (α : Type u) [LE α] extends Bot :

      An order is an OrderBot if it has a least element. We state this using a data mixin, holding the value of and the least element constraint.

      • bot : α
      • bot_le : ∀ (a : α), a

        is the least element

      Instances
        theorem OrderBot.bot_le {α : Type u} :
        ∀ {inst : LE α} [self : OrderBot α] (a : α), a

        is the least element

        noncomputable def botOrderOrNoBotOrder (α : Type u_3) [LE α] :

        An order is (noncomputably) either an OrderBot or a NoBotOrder. Use as casesI botOrderOrNoBotOrder α.

        Equations
        Instances For
          @[simp]
          theorem bot_le {α : Type u} [LE α] [OrderBot α] {a : α} :
          @[simp]
          theorem isBot_bot {α : Type u} [LE α] [OrderBot α] :
          instance OrderDual.instTop (α : Type u) [Bot α] :
          Equations
          instance OrderDual.instBot (α : Type u) [Top α] :
          Equations
          @[simp]
          theorem OrderDual.ofDual_bot (α : Type u) [Top α] :
          OrderDual.ofDual =
          @[simp]
          theorem OrderDual.ofDual_top (α : Type u) [Bot α] :
          OrderDual.ofDual =
          @[simp]
          theorem OrderDual.toDual_bot (α : Type u) [Bot α] :
          OrderDual.toDual =
          @[simp]
          theorem OrderDual.toDual_top (α : Type u) [Top α] :
          OrderDual.toDual =
          @[simp]
          theorem isMin_bot {α : Type u} [Preorder α] [OrderBot α] :
          @[simp]
          theorem not_lt_bot {α : Type u} [Preorder α] [OrderBot α] {a : α} :
          theorem ne_bot_of_gt {α : Type u} [Preorder α] [OrderBot α] {a : α} {b : α} (h : a < b) :
          theorem LT.lt.ne_bot {α : Type u} [Preorder α] [OrderBot α] {a : α} {b : α} (h : a < b) :

          Alias of ne_bot_of_gt.

          theorem bot_lt_of_lt {α : Type u} [Preorder α] [OrderBot α] {a : α} {b : α} (h : a < b) :
          < b
          theorem LT.lt.bot_lt {α : Type u} [Preorder α] [OrderBot α] {a : α} {b : α} (h : a < b) :
          < b

          Alias of bot_lt_of_lt.

          @[simp]
          theorem isMin_iff_eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
          @[simp]
          theorem isBot_iff_eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
          theorem not_isMin_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
          theorem not_isBot_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
          theorem IsMin.eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
          IsMin aa =

          Alias of the forward direction of isMin_iff_eq_bot.

          theorem IsBot.eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
          IsBot aa =

          Alias of the forward direction of isBot_iff_eq_bot.

          @[simp]
          theorem le_bot_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
          theorem bot_unique {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : a ) :
          a =
          theorem eq_bot_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
          theorem eq_bot_mono {α : Type u} [PartialOrder α] [OrderBot α] {a : α} {b : α} (h : a b) (h₂ : b = ) :
          a =
          theorem bot_lt_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
          @[simp]
          theorem not_bot_lt_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
          theorem eq_bot_or_bot_lt {α : Type u} [PartialOrder α] [OrderBot α] (a : α) :
          a = < a
          theorem eq_bot_of_minimal {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : ∀ (b : α), ¬b < a) :
          a =
          theorem Ne.bot_lt {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : a ) :
          < a
          theorem Ne.bot_lt' {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : a) :
          < a
          theorem ne_bot_of_le_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} {b : α} (hb : b ) (hab : b a) :
          theorem StrictMono.apply_eq_bot_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderBot α] [Preorder β] {f : αβ} {a : α} (hf : StrictMono f) :
          f a = f a =
          theorem StrictAnti.apply_eq_bot_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderBot α] [Preorder β] {f : αβ} {a : α} (hf : StrictAnti f) :
          f a = f a =
          theorem bot_not_mem_iff {α : Type u} [PartialOrder α] [OrderBot α] {s : Set α} :
          ¬ s ∀ (x : α), x s < x
          theorem StrictMono.minimal_preimage_bot {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β] [OrderBot β] {f : αβ} (H : StrictMono f) {a : α} (h_bot : f a = ) (x : α) :
          a x
          theorem OrderBot.ext_bot {α : Type u_3} {hA : PartialOrder α} (A : OrderBot α) {hB : PartialOrder α} (B : OrderBot α) (H : ∀ (x y : α), x y x y) :
          theorem top_sup_eq {α : Type u} [SemilatticeSup α] [OrderTop α] (a : α) :
          theorem sup_top_eq {α : Type u} [SemilatticeSup α] [OrderTop α] (a : α) :
          theorem bot_sup_eq {α : Type u} [SemilatticeSup α] [OrderBot α] (a : α) :
          a = a
          theorem sup_bot_eq {α : Type u} [SemilatticeSup α] [OrderBot α] (a : α) :
          a = a
          @[simp]
          theorem sup_eq_bot_iff {α : Type u} [SemilatticeSup α] [OrderBot α] {a : α} {b : α} :
          a b = a = b =
          theorem top_inf_eq {α : Type u} [SemilatticeInf α] [OrderTop α] (a : α) :
          a = a
          theorem inf_top_eq {α : Type u} [SemilatticeInf α] [OrderTop α] (a : α) :
          a = a
          @[simp]
          theorem inf_eq_top_iff {α : Type u} [SemilatticeInf α] [OrderTop α] {a : α} {b : α} :
          a b = a = b =
          theorem bot_inf_eq {α : Type u} [SemilatticeInf α] [OrderBot α] (a : α) :
          theorem inf_bot_eq {α : Type u} [SemilatticeInf α] [OrderBot α] (a : α) :

          Bounded order #

          class BoundedOrder (α : Type u) [LE α] extends OrderTop , OrderBot :

          A bounded order describes an order (≤) with a top and bottom element, denoted and respectively.

            Instances
              Equations
              Equations
              • =
              Equations
              • =

              In this section we prove some properties about monotone and antitone operations on Prop #

              theorem monotone_and {α : Type u} [Preorder α] {p : αProp} {q : αProp} (m_p : Monotone p) (m_q : Monotone q) :
              Monotone fun (x : α) => p x q x
              theorem monotone_or {α : Type u} [Preorder α] {p : αProp} {q : αProp} (m_p : Monotone p) (m_q : Monotone q) :
              Monotone fun (x : α) => p x q x
              theorem monotone_le {α : Type u} [Preorder α] {x : α} :
              Monotone fun (x_1 : α) => x x_1
              theorem monotone_lt {α : Type u} [Preorder α] {x : α} :
              Monotone fun (x_1 : α) => x < x_1
              theorem antitone_le {α : Type u} [Preorder α] {x : α} :
              Antitone fun (x_1 : α) => x_1 x
              theorem antitone_lt {α : Type u} [Preorder α] {x : α} :
              Antitone fun (x_1 : α) => x_1 < x
              theorem Monotone.forall {α : Type u} {β : Type v} [Preorder α] {P : βαProp} (hP : ∀ (x : β), Monotone (P x)) :
              Monotone fun (y : α) => ∀ (x : β), P x y
              theorem Antitone.forall {α : Type u} {β : Type v} [Preorder α] {P : βαProp} (hP : ∀ (x : β), Antitone (P x)) :
              Antitone fun (y : α) => ∀ (x : β), P x y
              theorem Monotone.ball {α : Type u} {β : Type v} [Preorder α] {P : βαProp} {s : Set β} (hP : ∀ (x : β), x sMonotone (P x)) :
              Monotone fun (y : α) => ∀ (x : β), x sP x y
              theorem Antitone.ball {α : Type u} {β : Type v} [Preorder α] {P : βαProp} {s : Set β} (hP : ∀ (x : β), x sAntitone (P x)) :
              Antitone fun (y : α) => ∀ (x : β), x sP x y
              theorem Monotone.exists {α : Type u} {β : Type v} [Preorder α] {P : βαProp} (hP : ∀ (x : β), Monotone (P x)) :
              Monotone fun (y : α) => ∃ (x : β), P x y
              theorem Antitone.exists {α : Type u} {β : Type v} [Preorder α] {P : βαProp} (hP : ∀ (x : β), Antitone (P x)) :
              Antitone fun (y : α) => ∃ (x : β), P x y
              theorem forall_ge_iff {α : Type u} [Preorder α] {P : αProp} {x₀ : α} (hP : Monotone P) :
              (∀ (x : α), x x₀P x) P x₀
              theorem forall_le_iff {α : Type u} [Preorder α] {P : αProp} {x₀ : α} (hP : Antitone P) :
              (∀ (x : α), x x₀P x) P x₀
              theorem exists_ge_and_iff_exists {α : Type u} [SemilatticeSup α] {P : αProp} {x₀ : α} (hP : Monotone P) :
              (∃ (x : α), x₀ x P x) ∃ (x : α), P x
              theorem exists_le_and_iff_exists {α : Type u} [SemilatticeInf α] {P : αProp} {x₀ : α} (hP : Antitone P) :
              (∃ (x : α), x x₀ P x) ∃ (x : α), P x

              Function lattices #

              instance Pi.instBotForall {ι : Type u_3} {α' : ιType u_4} [(i : ι) → Bot (α' i)] :
              Bot ((i : ι) → α' i)
              Equations
              • Pi.instBotForall = { bot := fun (x : ι) => }
              @[simp]
              theorem Pi.bot_apply {ι : Type u_3} {α' : ιType u_4} [(i : ι) → Bot (α' i)] (i : ι) :
              theorem Pi.bot_def {ι : Type u_3} {α' : ιType u_4} [(i : ι) → Bot (α' i)] :
              = fun (x : ι) =>
              instance Pi.instTopForall {ι : Type u_3} {α' : ιType u_4} [(i : ι) → Top (α' i)] :
              Top ((i : ι) → α' i)
              Equations
              • Pi.instTopForall = { top := fun (x : ι) => }
              @[simp]
              theorem Pi.top_apply {ι : Type u_3} {α' : ιType u_4} [(i : ι) → Top (α' i)] (i : ι) :
              theorem Pi.top_def {ι : Type u_3} {α' : ιType u_4} [(i : ι) → Top (α' i)] :
              = fun (x : ι) =>
              instance Pi.instOrderTop {ι : Type u_3} {α' : ιType u_4} [(i : ι) → LE (α' i)] [(i : ι) → OrderTop (α' i)] :
              OrderTop ((i : ι) → α' i)
              Equations
              instance Pi.instOrderBot {ι : Type u_3} {α' : ιType u_4} [(i : ι) → LE (α' i)] [(i : ι) → OrderBot (α' i)] :
              OrderBot ((i : ι) → α' i)
              Equations
              instance Pi.instBoundedOrder {ι : Type u_3} {α' : ιType u_4} [(i : ι) → LE (α' i)] [(i : ι) → BoundedOrder (α' i)] :
              BoundedOrder ((i : ι) → α' i)
              Equations
              • Pi.instBoundedOrder = BoundedOrder.mk
              theorem eq_bot_of_bot_eq_top {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : = ) (x : α) :
              x =
              theorem eq_top_of_bot_eq_top {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : = ) (x : α) :
              x =
              @[reducible, inline]
              abbrev OrderTop.lift {α : Type u} {β : Type v} [LE α] [Top α] [LE β] [OrderTop β] (f : αβ) (map_le : ∀ (a b : α), f a f ba b) (map_top : f = ) :

              Pullback an OrderTop.

              Equations
              Instances For
                @[reducible, inline]
                abbrev OrderBot.lift {α : Type u} {β : Type v} [LE α] [Bot α] [LE β] [OrderBot β] (f : αβ) (map_le : ∀ (a b : α), f a f ba b) (map_bot : f = ) :

                Pullback an OrderBot.

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev BoundedOrder.lift {α : Type u} {β : Type v} [LE α] [Top α] [Bot α] [LE β] [BoundedOrder β] (f : αβ) (map_le : ∀ (a b : α), f a f ba b) (map_top : f = ) (map_bot : f = ) :

                  Pullback a BoundedOrder.

                  Equations
                  Instances For

                    Subtype, order dual, product lattices #

                    @[reducible, inline]
                    abbrev Subtype.orderBot {α : Type u} {p : αProp} [LE α] [OrderBot α] (hbot : p ) :
                    OrderBot { x : α // p x }

                    A subtype remains a -order if the property holds at .

                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev Subtype.orderTop {α : Type u} {p : αProp} [LE α] [OrderTop α] (htop : p ) :
                      OrderTop { x : α // p x }

                      A subtype remains a -order if the property holds at .

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev Subtype.boundedOrder {α : Type u} {p : αProp} [LE α] [BoundedOrder α] (hbot : p ) (htop : p ) :

                        A subtype remains a bounded order if the property holds at and .

                        Equations
                        Instances For
                          @[simp]
                          theorem Subtype.mk_bot {α : Type u} {p : αProp} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ) :
                          , hbot =
                          @[simp]
                          theorem Subtype.mk_top {α : Type u} {p : αProp} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ) :
                          , htop =
                          theorem Subtype.coe_bot {α : Type u} {p : αProp} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ) :
                          =
                          theorem Subtype.coe_top {α : Type u} {p : αProp} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ) :
                          =
                          @[simp]
                          theorem Subtype.coe_eq_bot_iff {α : Type u} {p : αProp} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ) {x : { x : α // p x }} :
                          x = x =
                          @[simp]
                          theorem Subtype.coe_eq_top_iff {α : Type u} {p : αProp} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ) {x : { x : α // p x }} :
                          x = x =
                          @[simp]
                          theorem Subtype.mk_eq_bot_iff {α : Type u} {p : αProp} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ) {x : α} (hx : p x) :
                          x, hx = x =
                          @[simp]
                          theorem Subtype.mk_eq_top_iff {α : Type u} {p : αProp} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ) {x : α} (hx : p x) :
                          x, hx = x =
                          instance Prod.instTop (α : Type u) (β : Type v) [Top α] [Top β] :
                          Top (α × β)
                          Equations
                          instance Prod.instBot (α : Type u) (β : Type v) [Bot α] [Bot β] :
                          Bot (α × β)
                          Equations
                          theorem Prod.fst_top (α : Type u) (β : Type v) [Top α] [Top β] :
                          theorem Prod.snd_top (α : Type u) (β : Type v) [Top α] [Top β] :
                          theorem Prod.fst_bot (α : Type u) (β : Type v) [Bot α] [Bot β] :
                          theorem Prod.snd_bot (α : Type u) (β : Type v) [Bot α] [Bot β] :
                          instance Prod.instOrderTop (α : Type u) (β : Type v) [LE α] [LE β] [OrderTop α] [OrderTop β] :
                          OrderTop (α × β)
                          Equations
                          instance Prod.instOrderBot (α : Type u) (β : Type v) [LE α] [LE β] [OrderBot α] [OrderBot β] :
                          OrderBot (α × β)
                          Equations
                          instance Prod.instBoundedOrder (α : Type u) (β : Type v) [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] :
                          Equations
                          instance ULift.instTop {α : Type u} [Top α] :
                          Equations
                          • ULift.instTop = { top := { down := } }
                          @[simp]
                          theorem ULift.up_top {α : Type u} [Top α] :
                          { down := } =
                          @[simp]
                          theorem ULift.down_top {α : Type u} [Top α] :
                          .down =
                          instance ULift.instBot {α : Type u} [Bot α] :
                          Equations
                          • ULift.instBot = { bot := { down := } }
                          @[simp]
                          theorem ULift.up_bot {α : Type u} [Bot α] :
                          { down := } =
                          @[simp]
                          theorem ULift.down_bot {α : Type u} [Bot α] :
                          .down =
                          instance ULift.instOrderBot {α : Type u} [LE α] [OrderBot α] :
                          Equations
                          instance ULift.instOrderTop {α : Type u} [LE α] [OrderTop α] :
                          Equations
                          Equations
                          • ULift.instBoundedOrder = BoundedOrder.mk
                          theorem min_bot_left {α : Type u} [LinearOrder α] [OrderBot α] (a : α) :
                          theorem max_top_left {α : Type u} [LinearOrder α] [OrderTop α] (a : α) :
                          theorem min_top_left {α : Type u} [LinearOrder α] [OrderTop α] (a : α) :
                          min a = a
                          theorem max_bot_left {α : Type u} [LinearOrder α] [OrderBot α] (a : α) :
                          max a = a
                          theorem min_top_right {α : Type u} [LinearOrder α] [OrderTop α] (a : α) :
                          min a = a
                          theorem max_bot_right {α : Type u} [LinearOrder α] [OrderBot α] (a : α) :
                          max a = a
                          theorem min_bot_right {α : Type u} [LinearOrder α] [OrderBot α] (a : α) :
                          theorem max_top_right {α : Type u} [LinearOrder α] [OrderTop α] (a : α) :
                          @[simp]
                          theorem min_eq_bot {α : Type u} [LinearOrder α] [OrderBot α] {a : α} {b : α} :
                          min a b = a = b =
                          @[simp]
                          theorem max_eq_top {α : Type u} [LinearOrder α] [OrderTop α] {a : α} {b : α} :
                          max a b = a = b =
                          @[simp]
                          theorem max_eq_bot {α : Type u} [LinearOrder α] [OrderBot α] {a : α} {b : α} :
                          max a b = a = b =
                          @[simp]
                          theorem min_eq_top {α : Type u} [LinearOrder α] [OrderTop α] {a : α} {b : α} :
                          min a b = a = b =
                          @[simp]
                          theorem bot_ne_top {α : Type u} [PartialOrder α] [BoundedOrder α] [Nontrivial α] :
                          @[simp]
                          theorem top_ne_bot {α : Type u} [PartialOrder α] [BoundedOrder α] [Nontrivial α] :
                          @[simp]
                          theorem bot_lt_top {α : Type u} [PartialOrder α] [BoundedOrder α] [Nontrivial α] :
                          @[simp]
                          @[simp]