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 #

theorem Top.ext {α : Type u} (x : Top α) (y : Top α) (top : = ) :
x = y
theorem Top.ext_iff {α : Type u} (x : Top α) (y : Top α) :
x = y =
class Top (α : Type u) :
  • The top (⊤⊤, \top) element

    top : α

Typeclass for the ⊤⊤ (\top) notation

Instances
    theorem Bot.ext {α : Type u} (x : Bot α) (y : Bot α) (bot : = ) :
    x = y
    theorem Bot.ext_iff {α : Type u} (x : Bot α) (y : Bot α) :
    x = y =
    class Bot (α : Type u) :
    • The bot (⊥⊥, \bot) element

      bot : α

    Typeclass for the ⊥⊥ (\bot) notation

    Instances

      The top (⊤⊤, \top) element

      Equations

      The bot (⊥⊥, \bot) element

      Equations
      instance top_nonempty (α : Type u) [inst : Top α] :
      Equations
      instance bot_nonempty (α : Type u) [inst : Bot α] :
      Equations
      class OrderTop (α : Type u) [inst : LE α] extends Top :
      • ⊤⊤ is the greatest element

        le_top : ∀ (a : α), a

      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.

      Instances
        noncomputable def topOrderOrNoTopOrder (α : Type u_1) [inst : LE α] :

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

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

        Alias of ne_top_of_lt.

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

        Alias of the forward direction of isMax_iff_eq_top.

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

        Alias of the forward direction of isTop_iff_eq_top.

        @[simp]
        theorem top_le_iff {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :
        theorem top_unique {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} (h : a) :
        a =
        theorem eq_top_iff {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :
        theorem eq_top_mono {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} (h : a b) (h₂ : a = ) :
        b =
        theorem lt_top_iff_ne_top {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :
        @[simp]
        theorem not_lt_top_iff {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :
        theorem eq_top_or_lt_top {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] (a : α) :
        a = a <
        theorem Ne.lt_top {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} (h : a ) :
        a <
        theorem Ne.lt_top' {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} (h : a) :
        a <
        theorem ne_top_of_le_ne_top {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} (hb : b ) (hab : a b) :
        theorem StrictMono.apply_eq_top_iff {α : Type u} {β : Type v} [inst : PartialOrder α] [inst : OrderTop α] [inst : Preorder β] {f : αβ} {a : α} (hf : StrictMono f) :
        f a = f a =
        theorem StrictAnti.apply_eq_top_iff {α : Type u} {β : Type v} [inst : PartialOrder α] [inst : OrderTop α] [inst : Preorder β] {f : αβ} {a : α} (hf : StrictAnti f) :
        f a = f a =
        theorem not_isMin_top {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] [inst : Nontrivial α] :
        theorem StrictMono.maximal_preimage_top {α : Type u} {β : Type v} [inst : LinearOrder α] [inst : Preorder β] [inst : OrderTop β] {f : αβ} (H : StrictMono f) {a : α} (h_top : f a = ) (x : α) :
        x a
        theorem OrderTop.ext_top {α : Type u_1} {hA : PartialOrder α} (A : OrderTop α) {hB : PartialOrder α} (B : OrderTop α) (H : ∀ (x y : α), x y x y) :
        theorem OrderTop.ext {α : Type u_1} [inst : PartialOrder α] {A : OrderTop α} {B : OrderTop α} :
        A = B
        class OrderBot (α : Type u) [inst : LE α] extends Bot :
        • ⊥⊥ is the least element

          bot_le : ∀ (a : α), a

        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.

        Instances
          noncomputable def botOrderOrNoBotOrder (α : Type u_1) [inst : LE α] :

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

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

          Alias of ne_bot_of_gt.

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

          Alias of the forward direction of isMin_iff_eq_bot.

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

          Alias of the forward direction of isBot_iff_eq_bot.

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

          Bounded order #

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

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

            Instances
              instance OrderDual.boundedOrder (α : Type u) [inst : LE α] [inst : BoundedOrder α] :
              Equations
              theorem BoundedOrder.ext {α : Type u_1} [inst : PartialOrder α] {A : BoundedOrder α} {B : BoundedOrder α} :
              A = B

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

              theorem monotone_and {α : Type u} [inst : 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} [inst : 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} [inst : Preorder α] {x : α} :
              Monotone ((fun x x_1 => x x_1) x)
              theorem monotone_lt {α : Type u} [inst : Preorder α] {x : α} :
              Monotone ((fun x x_1 => x < x_1) x)
              theorem antitone_le {α : Type u} [inst : Preorder α] {x : α} :
              Antitone fun x => x x
              theorem antitone_lt {α : Type u} [inst : Preorder α] {x : α} :
              Antitone fun x => x < x
              theorem Monotone.forall {α : Type u} {β : Type v} [inst : Preorder α] {P : βαProp} (hP : ∀ (x : β), Monotone (P x)) :
              Monotone fun y => (x : β) → P x y
              theorem Antitone.forall {α : Type u} {β : Type v} [inst : Preorder α] {P : βαProp} (hP : ∀ (x : β), Antitone (P x)) :
              Antitone fun y => (x : β) → P x y
              theorem Monotone.ball {α : Type u} {β : Type v} [inst : 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} [inst : Preorder α] {P : βαProp} {s : Set β} (hP : ∀ (x : β), x sAntitone (P x)) :
              Antitone fun y => (x : β) → x sP x y
              theorem exists_ge_and_iff_exists {α : Type u} [inst : SemilatticeSup α] {P : αProp} {x₀ : α} (hP : Monotone P) :
              (x, x₀ x P x) x, P x
              theorem exists_le_and_iff_exists {α : Type u} [inst : SemilatticeInf α] {P : αProp} {x₀ : α} (hP : Antitone P) :
              (x, x x₀ P x) x, P x

              Function lattices #

              instance Pi.instBotForAll {ι : Type u_1} {α' : ιType u_2} [inst : (i : ι) → Bot (α' i)] :
              Bot ((i : ι) → α' i)
              Equations
              • Pi.instBotForAll = { bot := fun x => }
              @[simp]
              theorem Pi.bot_apply {ι : Type u_2} {α' : ιType u_1} [inst : (i : ι) → Bot (α' i)] (i : ι) :
              ((i : ι) → α' i) Pi.instBotForAll i =
              theorem Pi.bot_def {ι : Type u_2} {α' : ιType u_1} [inst : (i : ι) → Bot (α' i)] :
              = fun x =>
              instance Pi.instTopForAll {ι : Type u_1} {α' : ιType u_2} [inst : (i : ι) → Top (α' i)] :
              Top ((i : ι) → α' i)
              Equations
              • Pi.instTopForAll = { top := fun x => }
              @[simp]
              theorem Pi.top_apply {ι : Type u_2} {α' : ιType u_1} [inst : (i : ι) → Top (α' i)] (i : ι) :
              ((i : ι) → α' i) Pi.instTopForAll i =
              theorem Pi.top_def {ι : Type u_2} {α' : ιType u_1} [inst : (i : ι) → Top (α' i)] :
              = fun x =>
              instance Pi.orderTop {ι : Type u_1} {α' : ιType u_2} [inst : (i : ι) → LE (α' i)] [inst : (i : ι) → OrderTop (α' i)] :
              OrderTop ((i : ι) → α' i)
              Equations
              instance Pi.orderBot {ι : Type u_1} {α' : ιType u_2} [inst : (i : ι) → LE (α' i)] [inst : (i : ι) → OrderBot (α' i)] :
              OrderBot ((i : ι) → α' i)
              Equations
              instance Pi.boundedOrder {ι : Type u_1} {α' : ιType u_2} [inst : (i : ι) → LE (α' i)] [inst : (i : ι) → BoundedOrder (α' i)] :
              BoundedOrder ((i : ι) → α' i)
              Equations
              theorem eq_bot_of_bot_eq_top {α : Type u} [inst : PartialOrder α] [inst : BoundedOrder α] (hα : = ) (x : α) :
              x =
              theorem eq_top_of_bot_eq_top {α : Type u} [inst : PartialOrder α] [inst : BoundedOrder α] (hα : = ) (x : α) :
              x =
              theorem subsingleton_of_top_le_bot {α : Type u} [inst : PartialOrder α] [inst : BoundedOrder α] (h : ) :
              theorem subsingleton_of_bot_eq_top {α : Type u} [inst : PartialOrder α] [inst : BoundedOrder α] (hα : = ) :
              def OrderTop.lift {α : Type u} {β : Type v} [inst : LE α] [inst : Top α] [inst : LE β] [inst : OrderTop β] (f : αβ) (map_le : ∀ (a b : α), f a f ba b) (map_top : f = ) :

              Pullback an OrderTop.

              Equations
              def OrderBot.lift {α : Type u} {β : Type v} [inst : LE α] [inst : Bot α] [inst : LE β] [inst : OrderBot β] (f : αβ) (map_le : ∀ (a b : α), f a f ba b) (map_bot : f = ) :

              Pullback an OrderBot.

              Equations
              def BoundedOrder.lift {α : Type u} {β : Type v} [inst : LE α] [inst : Top α] [inst : Bot α] [inst : LE β] [inst : BoundedOrder β] (f : αβ) (map_le : ∀ (a b : α), f a f ba b) (map_top : f = ) (map_bot : f = ) :

              Pullback a BoundedOrder.

              Equations

              Subtype, order dual, product lattices #

              def Subtype.orderBot {α : Type u} {p : αProp} [inst : LE α] [inst : OrderBot α] (hbot : p ) :
              OrderBot { x // p x }

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

              Equations
              def Subtype.orderTop {α : Type u} {p : αProp} [inst : LE α] [inst : OrderTop α] (htop : p ) :
              OrderTop { x // p x }

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

              Equations
              def Subtype.boundedOrder {α : Type u} {p : αProp} [inst : LE α] [inst : BoundedOrder α] (hbot : p ) (htop : p ) :

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

              Equations
              @[simp]
              theorem Subtype.mk_bot {α : Type u} {p : αProp} [inst : PartialOrder α] [inst : OrderBot α] [inst : OrderBot (Subtype p)] (hbot : p ) :
              { val := , property := hbot } =
              @[simp]
              theorem Subtype.mk_top {α : Type u} {p : αProp} [inst : PartialOrder α] [inst : OrderTop α] [inst : OrderTop (Subtype p)] (htop : p ) :
              { val := , property := htop } =
              theorem Subtype.coe_bot {α : Type u} {p : αProp} [inst : PartialOrder α] [inst : OrderBot α] [inst : OrderBot (Subtype p)] (hbot : p ) :
              =
              theorem Subtype.coe_top {α : Type u} {p : αProp} [inst : PartialOrder α] [inst : OrderTop α] [inst : OrderTop (Subtype p)] (htop : p ) :
              =
              @[simp]
              theorem Subtype.coe_eq_bot_iff {α : Type u} {p : αProp} [inst : PartialOrder α] [inst : OrderBot α] [inst : OrderBot (Subtype p)] (hbot : p ) {x : { x // p x }} :
              x = x =
              @[simp]
              theorem Subtype.coe_eq_top_iff {α : Type u} {p : αProp} [inst : PartialOrder α] [inst : OrderTop α] [inst : OrderTop (Subtype p)] (htop : p ) {x : { x // p x }} :
              x = x =
              @[simp]
              theorem Subtype.mk_eq_bot_iff {α : Type u} {p : αProp} [inst : PartialOrder α] [inst : OrderBot α] [inst : OrderBot (Subtype p)] (hbot : p ) {x : α} (hx : p x) :
              { val := x, property := hx } = x =
              @[simp]
              theorem Subtype.mk_eq_top_iff {α : Type u} {p : αProp} [inst : PartialOrder α] [inst : OrderTop α] [inst : OrderTop (Subtype p)] (htop : p ) {x : α} (hx : p x) :
              { val := x, property := hx } = x =
              instance Prod.top (α : Type u) (β : Type v) [inst : Top α] [inst : Top β] :
              Top (α × β)
              Equations
              instance Prod.bot (α : Type u) (β : Type v) [inst : Bot α] [inst : Bot β] :
              Bot (α × β)
              Equations
              instance Prod.orderTop (α : Type u) (β : Type v) [inst : LE α] [inst : LE β] [inst : OrderTop α] [inst : OrderTop β] :
              OrderTop (α × β)
              Equations
              instance Prod.orderBot (α : Type u) (β : Type v) [inst : LE α] [inst : LE β] [inst : OrderBot α] [inst : OrderBot β] :
              OrderBot (α × β)
              Equations
              instance Prod.boundedOrder (α : Type u) (β : Type v) [inst : LE α] [inst : LE β] [inst : BoundedOrder α] [inst : BoundedOrder β] :
              Equations
              theorem min_bot_left {α : Type u} [inst : LinearOrder α] [inst : OrderBot α] (a : α) :
              theorem max_top_left {α : Type u} [inst : LinearOrder α] [inst : OrderTop α] (a : α) :
              theorem min_top_left {α : Type u} [inst : LinearOrder α] [inst : OrderTop α] (a : α) :
              min a = a
              theorem max_bot_left {α : Type u} [inst : LinearOrder α] [inst : OrderBot α] (a : α) :
              max a = a
              theorem min_top_right {α : Type u} [inst : LinearOrder α] [inst : OrderTop α] (a : α) :
              min a = a
              theorem max_bot_right {α : Type u} [inst : LinearOrder α] [inst : OrderBot α] (a : α) :
              max a = a
              theorem min_bot_right {α : Type u} [inst : LinearOrder α] [inst : OrderBot α] (a : α) :
              theorem max_top_right {α : Type u} [inst : LinearOrder α] [inst : OrderTop α] (a : α) :
              @[simp]
              theorem min_eq_bot {α : Type u} [inst : LinearOrder α] [inst : OrderBot α] {a : α} {b : α} :
              min a b = a = b =
              @[simp]
              theorem max_eq_top {α : Type u} [inst : LinearOrder α] [inst : OrderTop α] {a : α} {b : α} :
              max a b = a = b =
              @[simp]
              theorem max_eq_bot {α : Type u} [inst : LinearOrder α] [inst : OrderBot α] {a : α} {b : α} :
              max a b = a = b =
              @[simp]
              theorem min_eq_top {α : Type u} [inst : LinearOrder α] [inst : OrderTop α] {a : α} {b : α} :
              min a b = a = b =
              @[simp]
              theorem bot_ne_top {α : Type u} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : Nontrivial α] :
              @[simp]
              theorem top_ne_bot {α : Type u} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : Nontrivial α] :
              @[simp]
              theorem bot_lt_top {α : Type u} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : Nontrivial α] :
              @[simp]
              @[simp]