Documentation

Mathlib.Order.WithBot

WithBot, WithTop #

Adding a bot or a top to an order.

Main declarations #

@[simp]
theorem WithBot.coe_inj {α : Type u_1} {a b : α} :
a = b a = b
theorem WithBot.forall {α : Type u_1} {p : WithBot αProp} :
(∀ (x : WithBot α), p x) p ∀ (x : α), p x
theorem WithBot.exists {α : Type u_1} {p : WithBot αProp} :
( (x : WithBot α), p x) p (x : α), p x
theorem WithBot.some_eq_coe {α : Type u_1} (a : α) :
Option.some a = a
@[simp]
theorem WithBot.bot_ne_coe {α : Type u_1} {a : α} :
a
@[simp]
theorem WithBot.coe_ne_bot {α : Type u_1} {a : α} :
a
def WithBot.unbotD {α : Type u_1} (d : α) (x : WithBot α) :
α

Specialization of Option.getD to values in WithBot α that respects API boundaries.

Equations
    Instances For
      @[deprecated WithBot.unbotD (since := "2025-02-06")]
      def WithBot.unbot' {α : Type u_1} (d : α) (x : WithBot α) :
      α

      Alias of WithBot.unbotD.


      Specialization of Option.getD to values in WithBot α that respects API boundaries.

      Equations
        Instances For
          @[simp]
          theorem WithBot.unbotD_bot {α : Type u_5} (d : α) :
          @[deprecated WithBot.unbotD_bot (since := "2025-02-06")]
          theorem WithBot.unbot'_bot {α : Type u_5} (d : α) :

          Alias of WithBot.unbotD_bot.

          @[simp]
          theorem WithBot.unbotD_coe {α : Type u_5} (d x : α) :
          unbotD d x = x
          @[deprecated WithBot.unbotD_coe (since := "2025-02-06")]
          theorem WithBot.unbot'_coe {α : Type u_5} (d x : α) :
          unbotD d x = x

          Alias of WithBot.unbotD_coe.

          theorem WithBot.coe_eq_coe {α : Type u_1} {a b : α} :
          a = b a = b
          theorem WithBot.unbotD_eq_iff {α : Type u_1} {d y : α} {x : WithBot α} :
          unbotD d x = y x = y x = y = d
          @[deprecated WithBot.unbotD_eq_iff (since := "2025-02-06")]
          theorem WithBot.unbot'_eq_iff {α : Type u_1} {d y : α} {x : WithBot α} :
          unbotD d x = y x = y x = y = d

          Alias of WithBot.unbotD_eq_iff.

          @[simp]
          theorem WithBot.unbotD_eq_self_iff {α : Type u_1} {d : α} {x : WithBot α} :
          unbotD d x = d x = d x =
          @[deprecated WithBot.unbotD_eq_self_iff (since := "2025-02-06")]
          theorem WithBot.unbot'_eq_self_iff {α : Type u_1} {d : α} {x : WithBot α} :
          unbotD d x = d x = d x =

          Alias of WithBot.unbotD_eq_self_iff.

          theorem WithBot.unbotD_eq_unbotD_iff {α : Type u_1} {d : α} {x y : WithBot α} :
          unbotD d x = unbotD d y x = y x = d y = x = y = d
          @[deprecated WithBot.unbotD_eq_unbotD_iff (since := "2025-02-06")]
          theorem WithBot.unbot'_eq_unbot'_iff {α : Type u_1} {d : α} {x y : WithBot α} :
          unbotD d x = unbotD d y x = y x = d y = x = y = d

          Alias of WithBot.unbotD_eq_unbotD_iff.

          def WithBot.map {α : Type u_1} {β : Type u_2} (f : αβ) :
          WithBot αWithBot β

          Lift a map f : α → β to WithBot α → WithBot β. Implemented using Option.map.

          Equations
            Instances For
              @[simp]
              theorem WithBot.map_bot {α : Type u_1} {β : Type u_2} (f : αβ) :
              @[simp]
              theorem WithBot.map_coe {α : Type u_1} {β : Type u_2} (f : αβ) (a : α) :
              map f a = (f a)
              @[simp]
              theorem WithBot.map_eq_bot_iff {α : Type u_1} {β : Type u_2} {f : αβ} {a : WithBot α} :
              map f a = a =
              theorem WithBot.map_eq_some_iff {α : Type u_1} {β : Type u_2} {f : αβ} {y : β} {v : WithBot α} :
              map f v = y (x : α), v = x f x = y
              theorem WithBot.some_eq_map_iff {α : Type u_1} {β : Type u_2} {f : αβ} {y : β} {v : WithBot α} :
              y = map f v (x : α), v = x f x = y
              theorem WithBot.map_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : αβ} {f₂ : αγ} {g₁ : βδ} {g₂ : γδ} (h : g₁ f₁ = g₂ f₂) (a : α) :
              map g₁ (map f₁ a) = map g₂ (map f₂ a)
              def WithBot.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
              (αβγ)WithBot αWithBot βWithBot γ

              The image of a binary function f : α → β → γ as a function WithBot α → WithBot β → WithBot γ.

              Mathematically this should be thought of as the image of the corresponding function α × β → γ.

              Equations
                Instances For
                  theorem WithBot.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : β) :
                  map₂ f a b = (f a b)
                  @[simp]
                  theorem WithBot.map₂_bot_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (b : WithBot β) :
                  @[simp]
                  theorem WithBot.map₂_bot_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : WithBot α) :
                  @[simp]
                  theorem WithBot.map₂_coe_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : WithBot β) :
                  map₂ f (↑a) b = map (fun (b : β) => f a b) b
                  @[simp]
                  theorem WithBot.map₂_coe_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : WithBot α) (b : β) :
                  map₂ f a b = map (fun (x : α) => f x b) a
                  @[simp]
                  theorem WithBot.map₂_eq_bot_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {a : WithBot α} {b : WithBot β} :
                  map₂ f a b = a = b =
                  theorem WithBot.ne_bot_iff_exists {α : Type u_1} {x : WithBot α} :
                  x (a : α), a = x
                  theorem WithBot.eq_bot_iff_forall_ne {α : Type u_1} {x : WithBot α} :
                  x = ∀ (a : α), a x
                  @[deprecated WithBot.eq_bot_iff_forall_ne (since := "2025-03-19")]
                  theorem WithBot.forall_ne_iff_eq_bot {α : Type u_1} {x : WithBot α} :
                  x = ∀ (a : α), a x

                  Alias of WithBot.eq_bot_iff_forall_ne.

                  def WithBot.unbot {α : Type u_1} (x : WithBot α) :
                  x α

                  Deconstruct a x : WithBot α to the underlying value in α, given a proof that x ≠ ⊥.

                  Equations
                    Instances For
                      @[simp]
                      theorem WithBot.coe_unbot {α : Type u_1} (x : WithBot α) (hx : x ) :
                      (x.unbot hx) = x
                      @[simp]
                      theorem WithBot.unbot_coe {α : Type u_1} (x : α) (h : x := ) :
                      (↑x).unbot h = x
                      instance WithBot.canLift {α : Type u_1} :
                      CanLift (WithBot α) α some fun (r : WithBot α) => r
                      instance WithBot.instTop {α : Type u_1} [Top α] :
                      Equations
                        @[simp]
                        theorem WithBot.coe_top {α : Type u_1} [Top α] :
                        =
                        @[simp]
                        theorem WithBot.coe_eq_top {α : Type u_1} [Top α] {a : α} :
                        a = a =
                        @[simp]
                        theorem WithBot.top_eq_coe {α : Type u_1} [Top α] {a : α} :
                        = a = a
                        theorem WithBot.unbot_eq_iff {α : Type u_1} {a : WithBot α} {b : α} (h : a ) :
                        a.unbot h = b a = b
                        theorem WithBot.eq_unbot_iff {α : Type u_1} {a : α} {b : WithBot α} (h : b ) :
                        a = b.unbot h a = b
                        def Equiv.withBotSubtypeNe {α : Type u_1} :
                        { y : WithBot α // y } α

                        The equivalence between the non-bottom elements of WithBot α and α.

                        Equations
                          Instances For
                            @[simp]
                            theorem Equiv.withBotSubtypeNe_symm_apply_coe {α : Type u_1} (x : α) :
                            (withBotSubtypeNe.symm x) = x
                            @[simp]
                            theorem Equiv.withBotSubtypeNe_apply {α : Type u_1} (x✝ : { y : WithBot α // y }) :
                            withBotSubtypeNe x✝ = match x✝ with | x, h => x.unbot h
                            @[instance 10]
                            instance WithBot.le {α : Type u_1} [LE α] :
                            LE (WithBot α)
                            Equations
                              theorem WithBot.le_def {α : Type u_1} [LE α] {x y : WithBot α} :
                              x y ∀ (a : α), x = a (b : α), y = b a b
                              @[simp]
                              theorem WithBot.coe_le_coe {α : Type u_1} {a b : α} [LE α] :
                              a b a b
                              theorem WithBot.not_coe_le_bot {α : Type u_1} [LE α] (a : α) :
                              ¬a
                              instance WithBot.orderBot {α : Type u_1} [LE α] :
                              Equations
                                instance WithBot.orderTop {α : Type u_1} [LE α] [OrderTop α] :
                                Equations
                                  instance WithBot.instBoundedOrder {α : Type u_1} [LE α] [OrderTop α] :
                                  Equations
                                    @[simp]
                                    theorem WithBot.le_bot_iff {α : Type u_1} [LE α] {a : WithBot α} :

                                    There is a general version le_bot_iff, but this lemma does not require a PartialOrder.

                                    theorem WithBot.coe_le {α : Type u_1} {a b : α} [LE α] {o : Option α} :
                                    b o → (a o a b)
                                    theorem WithBot.coe_le_iff {α : Type u_1} {a : α} [LE α] {x : WithBot α} :
                                    a x (b : α), x = b a b
                                    theorem WithBot.le_coe_iff {α : Type u_1} {b : α} [LE α] {x : WithBot α} :
                                    x b ∀ (a : α), x = aa b
                                    theorem IsMax.withBot {α : Type u_1} {a : α} [LE α] (h : IsMax a) :
                                    IsMax a
                                    theorem WithBot.le_unbot_iff {α : Type u_1} {a : α} [LE α] {y : WithBot α} (hy : y ) :
                                    a y.unbot hy a y
                                    theorem WithBot.unbot_le_iff {α : Type u_1} {b : α} [LE α] {x : WithBot α} (hx : x ) :
                                    x.unbot hx b x b
                                    theorem WithBot.unbotD_le_iff {α : Type u_1} {a b : α} [LE α] {x : WithBot α} (hx : x = a b) :
                                    unbotD a x b x b
                                    @[deprecated WithBot.unbotD_le_iff (since := "2025-02-06")]
                                    theorem WithBot.unbot'_le_iff {α : Type u_1} {a b : α} [LE α] {x : WithBot α} (hx : x = a b) :
                                    unbotD a x b x b

                                    Alias of WithBot.unbotD_le_iff.

                                    @[instance 10]
                                    instance WithBot.lt {α : Type u_1} [LT α] :
                                    LT (WithBot α)
                                    Equations
                                      theorem WithBot.lt_def {α : Type u_1} [LT α] {x y : WithBot α} :
                                      x < y (b : α), y = b ∀ (a : α), x = aa < b
                                      @[simp]
                                      theorem WithBot.coe_lt_coe {α : Type u_1} {a b : α} [LT α] :
                                      a < b a < b
                                      @[simp]
                                      theorem WithBot.bot_lt_coe {α : Type u_1} [LT α] (a : α) :
                                      < a
                                      @[simp]
                                      theorem WithBot.not_lt_bot {α : Type u_1} [LT α] (a : WithBot α) :
                                      theorem WithBot.lt_iff_exists_coe {α : Type u_1} [LT α] {x y : WithBot α} :
                                      x < y (b : α), y = b x < b
                                      theorem WithBot.lt_coe_iff {α : Type u_1} {b : α} [LT α] {x : WithBot α} :
                                      x < b ∀ (a : α), x = aa < b
                                      theorem WithBot.bot_lt_iff_ne_bot {α : Type u_1} [LT α] {x : WithBot α} :

                                      A version of bot_lt_iff_ne_bot for WithBot that only requires LT α, not PartialOrder α.

                                      theorem WithBot.lt_unbot_iff {α : Type u_1} {a : α} [LT α] {y : WithBot α} (hy : y ) :
                                      a < y.unbot hy a < y
                                      theorem WithBot.unbot_lt_iff {α : Type u_1} {b : α} [LT α] {x : WithBot α} (hx : x ) :
                                      x.unbot hx < b x < b
                                      theorem WithBot.unbotD_lt_iff {α : Type u_1} {a b : α} [LT α] {x : WithBot α} (hx : x = a < b) :
                                      unbotD a x < b x < b
                                      @[deprecated WithBot.unbotD_lt_iff (since := "2025-02-06")]
                                      theorem WithBot.unbot'_lt_iff {α : Type u_1} {a b : α} [LT α] {x : WithBot α} (hx : x = a < b) :
                                      unbotD a x < b x < b

                                      Alias of WithBot.unbotD_lt_iff.

                                      instance WithBot.preorder {α : Type u_1} [Preorder α] :
                                      Equations
                                        Equations
                                          theorem WithBot.coe_strictMono {α : Type u_1} [Preorder α] :
                                          StrictMono fun (a : α) => a
                                          theorem WithBot.coe_mono {α : Type u_1} [Preorder α] :
                                          Monotone fun (a : α) => a
                                          theorem WithBot.monotone_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : WithBot αβ} :
                                          Monotone f (Monotone fun (a : α) => f a) ∀ (x : α), f f x
                                          @[simp]
                                          theorem WithBot.monotone_map_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} :
                                          theorem Monotone.withBot_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} :

                                          Alias of the reverse direction of WithBot.monotone_map_iff.

                                          theorem WithBot.strictMono_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : WithBot αβ} :
                                          StrictMono f (StrictMono fun (a : α) => f a) ∀ (x : α), f < f x
                                          theorem WithBot.strictAnti_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : WithBot αβ} :
                                          StrictAnti f (StrictAnti fun (a : α) => f a) ∀ (x : α), f x < f
                                          @[simp]
                                          theorem WithBot.strictMono_map_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} :
                                          theorem StrictMono.withBot_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} :

                                          Alias of the reverse direction of WithBot.strictMono_map_iff.

                                          theorem WithBot.map_le_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x y : WithBot α} (f : αβ) (mono_iff : ∀ {a b : α}, f a f b a b) :
                                          map f x map f y x y
                                          theorem WithBot.le_coe_unbotD {α : Type u_1} [Preorder α] (x : WithBot α) (b : α) :
                                          x (unbotD b x)
                                          @[deprecated WithBot.le_coe_unbotD (since := "2025-02-06")]
                                          theorem WithBot.le_coe_unbot' {α : Type u_1} [Preorder α] (x : WithBot α) (b : α) :
                                          x (unbotD b x)

                                          Alias of WithBot.le_coe_unbotD.

                                          @[simp]
                                          theorem WithBot.lt_coe_bot {α : Type u_1} [Preorder α] {x : WithBot α} [OrderBot α] :
                                          x < x =
                                          theorem WithBot.eq_bot_iff_forall_lt {α : Type u_1} [Preorder α] {x : WithBot α} :
                                          x = ∀ (b : α), x < b
                                          theorem WithBot.eq_bot_iff_forall_le {α : Type u_1} [Preorder α] {x : WithBot α} [NoBotOrder α] :
                                          x = ∀ (b : α), x b
                                          @[deprecated WithBot.eq_bot_iff_forall_lt (since := "2025-03-19")]
                                          theorem WithBot.forall_lt_iff_eq_bot {α : Type u_1} [Preorder α] {x : WithBot α} :
                                          x = ∀ (b : α), x < b

                                          Alias of WithBot.eq_bot_iff_forall_lt.

                                          @[deprecated WithBot.eq_bot_iff_forall_le (since := "2025-03-19")]
                                          theorem WithBot.forall_le_iff_eq_bot {α : Type u_1} [Preorder α] {x : WithBot α} [NoBotOrder α] :
                                          x = ∀ (b : α), x b

                                          Alias of WithBot.eq_bot_iff_forall_le.

                                          theorem WithBot.forall_le_coe_iff_le {α : Type u_1} [Preorder α] {x y : WithBot α} [NoBotOrder α] :
                                          (∀ (a : α), y ax a) x y
                                          theorem WithBot.eq_of_forall_le_coe_iff {α : Type u_1} [PartialOrder α] [NoBotOrder α] {x y : WithBot α} (h : ∀ (a : α), x a y a) :
                                          x = y
                                          theorem WithBot.coe_sup {α : Type u_1} [SemilatticeSup α] (a b : α) :
                                          (ab) = ab
                                          theorem WithBot.coe_inf {α : Type u_1} [SemilatticeInf α] (a b : α) :
                                          (ab) = ab
                                          instance WithBot.lattice {α : Type u_1} [Lattice α] :
                                          Equations
                                            instance WithBot.decidableEq {α : Type u_1} [DecidableEq α] :
                                            Equations
                                              instance WithBot.decidableLE {α : Type u_1} [LE α] [DecidableLE α] :
                                              Equations
                                                instance WithBot.decidableLT {α : Type u_1} [LT α] [DecidableLT α] :
                                                Equations
                                                  instance WithBot.isTotal_le {α : Type u_1} [LE α] [IsTotal α fun (x1 x2 : α) => x1 x2] :
                                                  IsTotal (WithBot α) fun (x1 x2 : WithBot α) => x1 x2
                                                  instance WithBot.linearOrder {α : Type u_1} [LinearOrder α] :
                                                  Equations
                                                    @[simp]
                                                    theorem WithBot.coe_min {α : Type u_1} [LinearOrder α] (a b : α) :
                                                    (min a b) = min a b
                                                    @[simp]
                                                    theorem WithBot.coe_max {α : Type u_1} [LinearOrder α] (a b : α) :
                                                    (max a b) = max a b
                                                    theorem WithBot.le_of_forall_lt_iff_le {α : Type u_1} [LinearOrder α] {x y : WithBot α} [DenselyOrdered α] [NoMinOrder α] :
                                                    (∀ (z : α), x < zy z) y x
                                                    theorem WithBot.ge_of_forall_gt_iff_ge {α : Type u_1} [LinearOrder α] {x y : WithBot α} [DenselyOrdered α] [NoMinOrder α] :
                                                    (∀ (z : α), z < xz y) x y
                                                    theorem WithBot.lt_iff_exists_coe_btwn {α : Type u_1} [Preorder α] [DenselyOrdered α] [NoMinOrder α] {a b : WithBot α} :
                                                    a < b (x : α), a < x x < b
                                                    instance WithBot.noTopOrder {α : Type u_1} [LE α] [NoTopOrder α] [Nonempty α] :
                                                    instance WithBot.noMaxOrder {α : Type u_1} [LT α] [NoMaxOrder α] [Nonempty α] :
                                                    theorem WithTop.coe_inj {α : Type u_1} {a b : α} :
                                                    a = b a = b
                                                    theorem WithTop.forall {α : Type u_1} {p : WithTop αProp} :
                                                    (∀ (x : WithTop α), p x) p ∀ (x : α), p x
                                                    theorem WithTop.exists {α : Type u_1} {p : WithTop αProp} :
                                                    ( (x : WithTop α), p x) p (x : α), p x
                                                    theorem WithTop.some_eq_coe {α : Type u_1} (a : α) :
                                                    Option.some a = a
                                                    @[simp]
                                                    theorem WithTop.top_ne_coe {α : Type u_1} {a : α} :
                                                    a
                                                    @[simp]
                                                    theorem WithTop.coe_ne_top {α : Type u_1} {a : α} :
                                                    a

                                                    WithTop.toDual is the equivalence sending to and any a : α to toDual a : αᵒᵈ. See WithTop.toDualBotEquiv for the related order-iso.

                                                    Equations
                                                      Instances For

                                                        WithTop.ofDual is the equivalence sending to and any a : αᵒᵈ to ofDual a : α. See WithTop.toDualBotEquiv for the related order-iso.

                                                        Equations
                                                          Instances For

                                                            WithBot.toDual is the equivalence sending to and any a : α to toDual a : αᵒᵈ. See WithBot.toDual_top_equiv for the related order-iso.

                                                            Equations
                                                              Instances For

                                                                WithBot.ofDual is the equivalence sending to and any a : αᵒᵈ to ofDual a : α. See WithBot.ofDual_top_equiv for the related order-iso.

                                                                Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem WithTop.toDual_apply_coe {α : Type u_1} (a : α) :
                                                                    @[simp]
                                                                    theorem WithTop.ofDual_apply_coe {α : Type u_1} (a : αᵒᵈ) :
                                                                    def WithTop.untopD {α : Type u_1} (d : α) (x : WithTop α) :
                                                                    α

                                                                    Specialization of Option.getD to values in WithTop α that respects API boundaries.

                                                                    Equations
                                                                      Instances For
                                                                        @[deprecated WithTop.untopD (since := "2025-02-06")]
                                                                        def WithTop.untop' {α : Type u_1} (d : α) (x : WithTop α) :
                                                                        α

                                                                        Alias of WithTop.untopD.


                                                                        Specialization of Option.getD to values in WithTop α that respects API boundaries.

                                                                        Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem WithTop.untopD_top {α : Type u_5} (d : α) :
                                                                            @[deprecated WithTop.untopD_top (since := "2025-02-06")]
                                                                            theorem WithTop.untop'_top {α : Type u_5} (d : α) :

                                                                            Alias of WithTop.untopD_top.

                                                                            @[simp]
                                                                            theorem WithTop.untopD_coe {α : Type u_5} (d x : α) :
                                                                            untopD d x = x
                                                                            @[deprecated WithTop.untopD_coe (since := "2025-02-06")]
                                                                            theorem WithTop.untop'_coe {α : Type u_5} (d x : α) :
                                                                            untopD d x = x

                                                                            Alias of WithTop.untopD_coe.

                                                                            @[simp]
                                                                            theorem WithTop.coe_eq_coe {α : Type u_1} {a b : α} :
                                                                            a = b a = b
                                                                            theorem WithTop.untopD_eq_iff {α : Type u_1} {d y : α} {x : WithTop α} :
                                                                            untopD d x = y x = y x = y = d
                                                                            @[deprecated WithTop.untopD_eq_iff (since := "2025-02-06")]
                                                                            theorem WithTop.untop'_eq_iff {α : Type u_1} {d y : α} {x : WithTop α} :
                                                                            untopD d x = y x = y x = y = d

                                                                            Alias of WithTop.untopD_eq_iff.

                                                                            @[simp]
                                                                            theorem WithTop.untopD_eq_self_iff {α : Type u_1} {d : α} {x : WithTop α} :
                                                                            untopD d x = d x = d x =
                                                                            @[deprecated WithTop.untopD_eq_self_iff (since := "2025-02-06")]
                                                                            theorem WithTop.untop'_eq_self_iff {α : Type u_1} {d : α} {x : WithTop α} :
                                                                            untopD d x = d x = d x =

                                                                            Alias of WithTop.untopD_eq_self_iff.

                                                                            theorem WithTop.untopD_eq_untopD_iff {α : Type u_1} {d : α} {x y : WithTop α} :
                                                                            untopD d x = untopD d y x = y x = d y = x = y = d
                                                                            @[deprecated WithTop.untopD_eq_untopD_iff (since := "2025-02-06")]
                                                                            theorem WithTop.untop'_eq_untop'_iff {α : Type u_1} {d : α} {x y : WithTop α} :
                                                                            untopD d x = untopD d y x = y x = d y = x = y = d

                                                                            Alias of WithTop.untopD_eq_untopD_iff.

                                                                            def WithTop.map {α : Type u_1} {β : Type u_2} (f : αβ) :
                                                                            WithTop αWithTop β

                                                                            Lift a map f : α → β to WithTop α → WithTop β. Implemented using Option.map.

                                                                            Equations
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem WithTop.map_top {α : Type u_1} {β : Type u_2} (f : αβ) :
                                                                                @[simp]
                                                                                theorem WithTop.map_coe {α : Type u_1} {β : Type u_2} (f : αβ) (a : α) :
                                                                                map f a = (f a)
                                                                                @[simp]
                                                                                theorem WithTop.map_eq_top_iff {α : Type u_1} {β : Type u_2} {f : αβ} {a : WithTop α} :
                                                                                map f a = a =
                                                                                theorem WithTop.map_eq_some_iff {α : Type u_1} {β : Type u_2} {f : αβ} {y : β} {v : WithTop α} :
                                                                                map f v = y (x : α), v = x f x = y
                                                                                theorem WithTop.some_eq_map_iff {α : Type u_1} {β : Type u_2} {f : αβ} {y : β} {v : WithTop α} :
                                                                                y = map f v (x : α), v = x f x = y
                                                                                theorem WithTop.map_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : αβ} {f₂ : αγ} {g₁ : βδ} {g₂ : γδ} (h : g₁ f₁ = g₂ f₂) (a : α) :
                                                                                map g₁ (map f₁ a) = map g₂ (map f₂ a)
                                                                                def WithTop.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
                                                                                (αβγ)WithTop αWithTop βWithTop γ

                                                                                The image of a binary function f : α → β → γ as a function WithTop α → WithTop β → WithTop γ.

                                                                                Mathematically this should be thought of as the image of the corresponding function α × β → γ.

                                                                                Equations
                                                                                  Instances For
                                                                                    theorem WithTop.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : β) :
                                                                                    map₂ f a b = (f a b)
                                                                                    @[simp]
                                                                                    theorem WithTop.map₂_top_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (b : WithTop β) :
                                                                                    @[simp]
                                                                                    theorem WithTop.map₂_top_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : WithTop α) :
                                                                                    @[simp]
                                                                                    theorem WithTop.map₂_coe_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : WithTop β) :
                                                                                    map₂ f (↑a) b = map (fun (b : β) => f a b) b
                                                                                    @[simp]
                                                                                    theorem WithTop.map₂_coe_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : WithTop α) (b : β) :
                                                                                    map₂ f a b = map (fun (x : α) => f x b) a
                                                                                    @[simp]
                                                                                    theorem WithTop.map₂_eq_top_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {a : WithTop α} {b : WithTop β} :
                                                                                    map₂ f a b = a = b =
                                                                                    theorem WithTop.map_toDual {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : WithBot α) :
                                                                                    theorem WithTop.map_ofDual {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithBot αᵒᵈ) :
                                                                                    theorem WithTop.toDual_map {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithTop α) :
                                                                                    theorem WithTop.ne_top_iff_exists {α : Type u_1} {x : WithTop α} :
                                                                                    x (a : α), a = x
                                                                                    theorem WithTop.eq_top_iff_forall_ne {α : Type u_1} {x : WithTop α} :
                                                                                    x = ∀ (a : α), a x
                                                                                    @[deprecated WithTop.eq_top_iff_forall_ne (since := "2025-03-19")]
                                                                                    theorem WithTop.forall_ne_iff_eq_top {α : Type u_1} {x : WithTop α} :
                                                                                    x = ∀ (a : α), a x

                                                                                    Alias of WithTop.eq_top_iff_forall_ne.

                                                                                    def WithTop.untop {α : Type u_1} (x : WithTop α) :
                                                                                    x α

                                                                                    Deconstruct a x : WithTop α to the underlying value in α, given a proof that x ≠ ⊤.

                                                                                    Equations
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem WithTop.coe_untop {α : Type u_1} (x : WithTop α) (hx : x ) :
                                                                                        (x.untop hx) = x
                                                                                        @[simp]
                                                                                        theorem WithTop.untop_coe {α : Type u_1} (x : α) (h : x := ) :
                                                                                        (↑x).untop h = x
                                                                                        instance WithTop.canLift {α : Type u_1} :
                                                                                        CanLift (WithTop α) α some fun (r : WithTop α) => r
                                                                                        instance WithTop.instBot {α : Type u_1} [Bot α] :
                                                                                        Equations
                                                                                          @[simp]
                                                                                          theorem WithTop.coe_bot {α : Type u_1} [Bot α] :
                                                                                          =
                                                                                          @[simp]
                                                                                          theorem WithTop.coe_eq_bot {α : Type u_1} [Bot α] {a : α} :
                                                                                          a = a =
                                                                                          @[simp]
                                                                                          theorem WithTop.bot_eq_coe {α : Type u_1} [Bot α] {a : α} :
                                                                                          = a = a
                                                                                          theorem WithTop.untop_eq_iff {α : Type u_1} {a : WithTop α} {b : α} (h : a ) :
                                                                                          a.untop h = b a = b
                                                                                          theorem WithTop.eq_untop_iff {α : Type u_1} {a : α} {b : WithTop α} (h : b ) :
                                                                                          a = b.untop h a = b
                                                                                          def Equiv.withTopSubtypeNe {α : Type u_1} :
                                                                                          { y : WithTop α // y } α

                                                                                          The equivalence between the non-top elements of WithTop α and α.

                                                                                          Equations
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem Equiv.withTopSubtypeNe_apply {α : Type u_1} (x✝ : { y : WithTop α // y }) :
                                                                                              withTopSubtypeNe x✝ = match x✝ with | x, h => x.untop h
                                                                                              @[simp]
                                                                                              theorem Equiv.withTopSubtypeNe_symm_apply_coe {α : Type u_1} (x : α) :
                                                                                              (withTopSubtypeNe.symm x) = x
                                                                                              @[instance 10]
                                                                                              instance WithTop.le {α : Type u_1} [LE α] :
                                                                                              LE (WithTop α)
                                                                                              Equations
                                                                                                theorem WithTop.le_def {α : Type u_1} [LE α] {x y : WithTop α} :
                                                                                                x y ∀ (b : α), y = b (a : α), x = a a b
                                                                                                @[simp]
                                                                                                theorem WithTop.coe_le_coe {α : Type u_1} {a b : α} [LE α] :
                                                                                                a b a b
                                                                                                theorem WithTop.not_top_le_coe {α : Type u_1} [LE α] (a : α) :
                                                                                                ¬ a
                                                                                                instance WithTop.orderTop {α : Type u_1} [LE α] :
                                                                                                Equations
                                                                                                  instance WithTop.orderBot {α : Type u_1} [LE α] [OrderBot α] :
                                                                                                  Equations
                                                                                                    instance WithTop.boundedOrder {α : Type u_1} [LE α] [OrderBot α] :
                                                                                                    Equations
                                                                                                      @[simp]
                                                                                                      theorem WithTop.top_le_iff {α : Type u_1} [LE α] {a : WithTop α} :

                                                                                                      There is a general version top_le_iff, but this lemma does not require a PartialOrder.

                                                                                                      theorem WithTop.le_coe {α : Type u_1} {a b : α} [LE α] {o : Option α} :
                                                                                                      a o → (o b a b)
                                                                                                      theorem WithTop.le_coe_iff {α : Type u_1} {b : α} [LE α] {x : WithTop α} :
                                                                                                      x b (a : α), x = a a b
                                                                                                      theorem WithTop.coe_le_iff {α : Type u_1} {a : α} [LE α] {x : WithTop α} :
                                                                                                      a x ∀ (b : α), x = ba b
                                                                                                      theorem IsMin.withTop {α : Type u_1} {a : α} [LE α] (h : IsMin a) :
                                                                                                      IsMin a
                                                                                                      theorem WithTop.untop_le_iff {α : Type u_1} {b : α} [LE α] {x : WithTop α} (hx : x ) :
                                                                                                      x.untop hx b x b
                                                                                                      theorem WithTop.le_untop_iff {α : Type u_1} {a : α} [LE α] {y : WithTop α} (hy : y ) :
                                                                                                      a y.untop hy a y
                                                                                                      theorem WithTop.le_untopD_iff {α : Type u_1} {a b : α} [LE α] {y : WithTop α} (hy : y = a b) :
                                                                                                      a untopD b y a y
                                                                                                      @[deprecated WithTop.le_untopD_iff (since := "2025-02-11")]
                                                                                                      theorem WithTop.le_untop'_iff {α : Type u_1} {a b : α} [LE α] {y : WithTop α} (hy : y = a b) :
                                                                                                      a untopD b y a y

                                                                                                      Alias of WithTop.le_untopD_iff.

                                                                                                      @[instance 10]
                                                                                                      instance WithTop.lt {α : Type u_1} [LT α] :
                                                                                                      LT (WithTop α)
                                                                                                      Equations
                                                                                                        theorem WithTop.lt_def {α : Type u_1} [LT α] {x y : WithTop α} :
                                                                                                        x < y (a : α), x = a ∀ (b : α), y = ba < b
                                                                                                        @[simp]
                                                                                                        theorem WithTop.coe_lt_coe {α : Type u_1} {a b : α} [LT α] :
                                                                                                        a < b a < b
                                                                                                        @[simp]
                                                                                                        theorem WithTop.coe_lt_top {α : Type u_1} [LT α] (a : α) :
                                                                                                        a <
                                                                                                        @[simp]
                                                                                                        theorem WithTop.not_top_lt {α : Type u_1} [LT α] (a : WithTop α) :
                                                                                                        theorem WithTop.lt_iff_exists_coe {α : Type u_1} [LT α] {x y : WithTop α} :
                                                                                                        x < y (a : α), x = a a < y
                                                                                                        theorem WithTop.coe_lt_iff {α : Type u_1} {a : α} [LT α] {y : WithTop α} :
                                                                                                        a < y ∀ (b : α), y = ba < b
                                                                                                        theorem WithTop.lt_top_iff_ne_top {α : Type u_1} [LT α] {x : WithTop α} :

                                                                                                        A version of lt_top_iff_ne_top for WithTop that only requires LT α, not PartialOrder α.

                                                                                                        theorem WithTop.lt_untop_iff {α : Type u_1} {a : α} [LT α] {y : WithTop α} (hy : y ) :
                                                                                                        a < y.untop hy a < y
                                                                                                        theorem WithTop.untop_lt_iff {α : Type u_1} {b : α} [LT α] {x : WithTop α} (hx : x ) :
                                                                                                        x.untop hx < b x < b
                                                                                                        theorem WithTop.lt_untopD_iff {α : Type u_1} {a b : α} [LT α] {y : WithTop α} (hy : y = a < b) :
                                                                                                        a < untopD b y a < y
                                                                                                        @[deprecated WithTop.lt_untopD_iff (since := "2025-02-11")]
                                                                                                        theorem WithTop.lt_untop'_iff {α : Type u_1} {a b : α} [LT α] {y : WithTop α} (hy : y = a < b) :
                                                                                                        a < untopD b y a < y

                                                                                                        Alias of WithTop.lt_untopD_iff.

                                                                                                        instance WithTop.preorder {α : Type u_1} [Preorder α] :
                                                                                                        Equations
                                                                                                          Equations
                                                                                                            theorem WithTop.coe_strictMono {α : Type u_1} [Preorder α] :
                                                                                                            StrictMono fun (a : α) => a
                                                                                                            theorem WithTop.coe_mono {α : Type u_1} [Preorder α] :
                                                                                                            Monotone fun (a : α) => a
                                                                                                            theorem WithTop.monotone_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : WithTop αβ} :
                                                                                                            Monotone f (Monotone fun (a : α) => f a) ∀ (x : α), f x f
                                                                                                            @[simp]
                                                                                                            theorem WithTop.monotone_map_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} :
                                                                                                            theorem Monotone.withTop_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} :

                                                                                                            Alias of the reverse direction of WithTop.monotone_map_iff.

                                                                                                            theorem WithTop.strictMono_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : WithTop αβ} :
                                                                                                            StrictMono f (StrictMono fun (a : α) => f a) ∀ (x : α), f x < f
                                                                                                            theorem WithTop.strictAnti_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : WithTop αβ} :
                                                                                                            StrictAnti f (StrictAnti fun (a : α) => f a) ∀ (x : α), f < f x
                                                                                                            @[simp]
                                                                                                            theorem WithTop.strictMono_map_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} :
                                                                                                            theorem StrictMono.withTop_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} :

                                                                                                            Alias of the reverse direction of WithTop.strictMono_map_iff.

                                                                                                            theorem WithTop.map_le_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x y : WithTop α} (f : αβ) (mono_iff : ∀ {a b : α}, f a f b a b) :
                                                                                                            map f x map f y x y
                                                                                                            theorem WithTop.coe_untopD_le {α : Type u_1} [Preorder α] (y : WithTop α) (a : α) :
                                                                                                            (untopD a y) y
                                                                                                            @[deprecated WithTop.coe_untopD_le (since := "2025-02-11")]
                                                                                                            theorem WithTop.coe_untop'_le {α : Type u_1} [Preorder α] (y : WithTop α) (a : α) :
                                                                                                            (untopD a y) y

                                                                                                            Alias of WithTop.coe_untopD_le.

                                                                                                            @[simp]
                                                                                                            theorem WithTop.coe_top_lt {α : Type u_1} [Preorder α] {x : WithTop α} [OrderTop α] :
                                                                                                            < x x =
                                                                                                            theorem WithTop.eq_top_iff_forall_gt {α : Type u_1} [Preorder α] {y : WithTop α} :
                                                                                                            y = ∀ (a : α), a < y
                                                                                                            theorem WithTop.eq_top_iff_forall_ge {α : Type u_1} [Preorder α] {y : WithTop α} [NoTopOrder α] :
                                                                                                            y = ∀ (a : α), a y
                                                                                                            @[deprecated WithTop.eq_top_iff_forall_gt (since := "2025-03-19")]
                                                                                                            theorem WithTop.forall_gt_iff_eq_top {α : Type u_1} [Preorder α] {y : WithTop α} :
                                                                                                            y = ∀ (a : α), a < y

                                                                                                            Alias of WithTop.eq_top_iff_forall_gt.

                                                                                                            @[deprecated WithTop.eq_top_iff_forall_ge (since := "2025-03-19")]
                                                                                                            theorem WithTop.forall_ge_iff_eq_top {α : Type u_1} [Preorder α] {y : WithTop α} [NoTopOrder α] :
                                                                                                            y = ∀ (a : α), a y

                                                                                                            Alias of WithTop.eq_top_iff_forall_ge.

                                                                                                            theorem WithTop.forall_coe_le_iff_le {α : Type u_1} [Preorder α] {x y : WithTop α} [NoTopOrder α] :
                                                                                                            (∀ (a : α), a xa y) x y
                                                                                                            theorem WithTop.eq_of_forall_coe_le_iff {α : Type u_1} [PartialOrder α] [NoTopOrder α] {x y : WithTop α} (h : ∀ (a : α), a x a y) :
                                                                                                            x = y
                                                                                                            theorem WithTop.coe_inf {α : Type u_1} [SemilatticeInf α] (a b : α) :
                                                                                                            (ab) = ab
                                                                                                            theorem WithTop.coe_sup {α : Type u_1} [SemilatticeSup α] (a b : α) :
                                                                                                            (ab) = ab
                                                                                                            instance WithTop.lattice {α : Type u_1} [Lattice α] :
                                                                                                            Equations
                                                                                                              instance WithTop.decidableEq {α : Type u_1} [DecidableEq α] :
                                                                                                              Equations
                                                                                                                instance WithTop.decidableLE {α : Type u_1} [LE α] [DecidableLE α] :
                                                                                                                Equations
                                                                                                                  instance WithTop.decidableLT {α : Type u_1} [LT α] [DecidableLT α] :
                                                                                                                  Equations
                                                                                                                    instance WithTop.isTotal_le {α : Type u_1} [LE α] [IsTotal α fun (x1 x2 : α) => x1 x2] :
                                                                                                                    IsTotal (WithTop α) fun (x1 x2 : WithTop α) => x1 x2
                                                                                                                    instance WithTop.linearOrder {α : Type u_1} [LinearOrder α] :
                                                                                                                    Equations
                                                                                                                      @[simp]
                                                                                                                      theorem WithTop.coe_min {α : Type u_1} [LinearOrder α] (a b : α) :
                                                                                                                      (min a b) = min a b
                                                                                                                      @[simp]
                                                                                                                      theorem WithTop.coe_max {α : Type u_1} [LinearOrder α] (a b : α) :
                                                                                                                      (max a b) = max a b
                                                                                                                      theorem WithTop.le_of_forall_lt_iff_le {α : Type u_1} [LinearOrder α] {x y : WithTop α} [DenselyOrdered α] [NoMaxOrder α] :
                                                                                                                      (∀ (b : α), x < by b) y x
                                                                                                                      theorem WithTop.ge_of_forall_gt_iff_ge {α : Type u_1} [LinearOrder α] {x y : WithTop α} [DenselyOrdered α] [NoMaxOrder α] :
                                                                                                                      (∀ (a : α), a < xa y) x y
                                                                                                                      instance WithTop.trichotomous.lt {α : Type u_1} [Preorder α] [IsTrichotomous α fun (x1 x2 : α) => x1 < x2] :
                                                                                                                      IsTrichotomous (WithTop α) fun (x1 x2 : WithTop α) => x1 < x2
                                                                                                                      instance WithTop.IsWellOrder.lt {α : Type u_1} [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] :
                                                                                                                      IsWellOrder (WithTop α) fun (x1 x2 : WithTop α) => x1 < x2
                                                                                                                      instance WithTop.trichotomous.gt {α : Type u_1} [Preorder α] [IsTrichotomous α fun (x1 x2 : α) => x1 > x2] :
                                                                                                                      IsTrichotomous (WithTop α) fun (x1 x2 : WithTop α) => x1 > x2
                                                                                                                      instance WithTop.IsWellOrder.gt {α : Type u_1} [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 > x2] :
                                                                                                                      IsWellOrder (WithTop α) fun (x1 x2 : WithTop α) => x1 > x2
                                                                                                                      instance WithBot.trichotomous.lt {α : Type u_1} [Preorder α] [h : IsTrichotomous α fun (x1 x2 : α) => x1 < x2] :
                                                                                                                      IsTrichotomous (WithBot α) fun (x1 x2 : WithBot α) => x1 < x2
                                                                                                                      instance WithBot.isWellOrder.lt {α : Type u_1} [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] :
                                                                                                                      IsWellOrder (WithBot α) fun (x1 x2 : WithBot α) => x1 < x2
                                                                                                                      instance WithBot.trichotomous.gt {α : Type u_1} [Preorder α] [h : IsTrichotomous α fun (x1 x2 : α) => x1 > x2] :
                                                                                                                      IsTrichotomous (WithBot α) fun (x1 x2 : WithBot α) => x1 > x2
                                                                                                                      instance WithBot.isWellOrder.gt {α : Type u_1} [Preorder α] [h : IsWellOrder α fun (x1 x2 : α) => x1 > x2] :
                                                                                                                      IsWellOrder (WithBot α) fun (x1 x2 : WithBot α) => x1 > x2
                                                                                                                      theorem WithTop.lt_iff_exists_coe_btwn {α : Type u_1} [Preorder α] [DenselyOrdered α] [NoMaxOrder α] {a b : WithTop α} :
                                                                                                                      a < b (x : α), a < x x < b
                                                                                                                      instance WithTop.noBotOrder {α : Type u_1} [LE α] [NoBotOrder α] [Nonempty α] :
                                                                                                                      instance WithTop.noMinOrder {α : Type u_1} [LT α] [NoMinOrder α] [Nonempty α] :
                                                                                                                      theorem WithBot.eq_top_iff_forall_ge {α : Type u_1} [Preorder α] [Nonempty α] [NoTopOrder α] {x : WithBot (WithTop α)} :
                                                                                                                      x = ∀ (a : α), a x

                                                                                                                      (WithBot α)ᵒᵈ ≃ WithTop αᵒᵈ, (WithTop α)ᵒᵈ ≃ WithBot αᵒᵈ #

                                                                                                                      @[simp]
                                                                                                                      theorem WithBot.toDual_apply_coe {α : Type u_1} (a : α) :
                                                                                                                      @[simp]
                                                                                                                      theorem WithBot.ofDual_apply_coe {α : Type u_1} (a : αᵒᵈ) :
                                                                                                                      theorem WithBot.map_toDual {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : WithTop α) :
                                                                                                                      theorem WithBot.map_ofDual {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithTop αᵒᵈ) :
                                                                                                                      theorem WithBot.toDual_map {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithBot α) :
                                                                                                                      theorem WithBot.ofDual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : WithBot αᵒᵈ) :
                                                                                                                      theorem WithBot.toDual_le_iff {α : Type u_1} [LE α] {x : WithBot α} {y : WithTop αᵒᵈ} :
                                                                                                                      theorem WithBot.le_toDual_iff {α : Type u_1} [LE α] {x : WithTop αᵒᵈ} {y : WithBot α} :
                                                                                                                      @[simp]
                                                                                                                      theorem WithBot.toDual_le_toDual_iff {α : Type u_1} [LE α] {x y : WithBot α} :
                                                                                                                      theorem WithBot.ofDual_le_iff {α : Type u_1} [LE α] {x : WithBot αᵒᵈ} {y : WithTop α} :
                                                                                                                      theorem WithBot.le_ofDual_iff {α : Type u_1} [LE α] {x : WithTop α} {y : WithBot αᵒᵈ} :
                                                                                                                      @[simp]
                                                                                                                      theorem WithTop.toDual_le_iff {α : Type u_1} [LE α] {x : WithTop α} {y : WithBot αᵒᵈ} :
                                                                                                                      theorem WithTop.le_toDual_iff {α : Type u_1} [LE α] {x : WithBot αᵒᵈ} {y : WithTop α} :
                                                                                                                      @[simp]
                                                                                                                      theorem WithTop.toDual_le_toDual_iff {α : Type u_1} [LE α] {x y : WithTop α} :
                                                                                                                      theorem WithTop.ofDual_le_iff {α : Type u_1} [LE α] {x : WithTop αᵒᵈ} {y : WithBot α} :
                                                                                                                      theorem WithTop.le_ofDual_iff {α : Type u_1} [LE α] {x : WithBot α} {y : WithTop αᵒᵈ} :
                                                                                                                      @[simp]
                                                                                                                      theorem WithBot.toDual_lt_iff {α : Type u_1} [LT α] {x : WithBot α} {y : WithTop αᵒᵈ} :
                                                                                                                      theorem WithBot.lt_toDual_iff {α : Type u_1} [LT α] {x : WithTop αᵒᵈ} {y : WithBot α} :
                                                                                                                      @[simp]
                                                                                                                      theorem WithBot.toDual_lt_toDual_iff {α : Type u_1} [LT α] {x y : WithBot α} :
                                                                                                                      theorem WithBot.ofDual_lt_iff {α : Type u_1} [LT α] {x : WithBot αᵒᵈ} {y : WithTop α} :
                                                                                                                      theorem WithBot.lt_ofDual_iff {α : Type u_1} [LT α] {x : WithTop α} {y : WithBot αᵒᵈ} :
                                                                                                                      @[simp]
                                                                                                                      theorem WithTop.toDual_lt_iff {α : Type u_1} [LT α] {x : WithTop α} {y : WithBot αᵒᵈ} :
                                                                                                                      theorem WithTop.lt_toDual_iff {α : Type u_1} [LT α] {x : WithBot αᵒᵈ} {y : WithTop α} :
                                                                                                                      @[simp]
                                                                                                                      theorem WithTop.toDual_lt_toDual_iff {α : Type u_1} [LT α] {x y : WithTop α} :
                                                                                                                      theorem WithTop.ofDual_lt_iff {α : Type u_1} [LT α] {x : WithTop αᵒᵈ} {y : WithBot α} :
                                                                                                                      theorem WithTop.lt_ofDual_iff {α : Type u_1} [LT α] {x : WithBot α} {y : WithTop αᵒᵈ} :
                                                                                                                      @[simp]