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 : α} :
def WithBot.unbot' {α : Type u_1} (d : α) (x : WithBot α) :
α

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

Equations
Instances For
    @[simp]
    theorem WithBot.unbot'_bot {α : Type u_5} (d : α) :
    @[simp]
    theorem WithBot.unbot'_coe {α : Type u_5} (d x : α) :
    unbot' d x = x
    theorem WithBot.coe_eq_coe {α : Type u_1} {a b : α} :
    a = b a = b
    theorem WithBot.unbot'_eq_iff {α : Type u_1} {d y : α} {x : WithBot α} :
    unbot' d x = y x = y x = y = d
    @[simp]
    theorem WithBot.unbot'_eq_self_iff {α : Type u_1} {d : α} {x : WithBot α} :
    unbot' d x = d x = d x =
    theorem WithBot.unbot'_eq_unbot'_iff {α : Type u_1} {d : α} {x y : WithBot α} :
    unbot' d x = unbot' d y x = y x = d y = x = y = d
    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 α} :
      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 β} :
        theorem WithBot.ne_bot_iff_exists {α : Type u_1} {x : WithBot α} :
        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 ) :
          @[simp]
          theorem WithBot.unbot_coe {α : Type u_1} (x : α) (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 : α} :
          @[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 ) :
          def Equiv.withBotSubtypeNe {α : Type u_1} :

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

          Equations
          Instances For
            @[simp]
            @[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
            @[simp]
            theorem WithBot.coe_le_coe {α : Type u_1} {a b : α} [LE α] :
            instance WithBot.orderBot {α : Type u_1} [LE α] :
            Equations
            @[simp, deprecated WithBot.coe_le_coe "Don't mix Option and WithBot" (since := "2024-05-27")]
            theorem WithBot.some_le_some {α : Type u_1} {a b : α} [LE α] :
            @[simp, deprecated bot_le "Don't mix Option and WithBot" (since := "2024-05-27")]
            theorem WithBot.none_le {α : Type u_1} [LE α] {a : WithBot α} :
            instance WithBot.orderTop {α : Type u_1} [LE α] [OrderTop α] :
            Equations
            theorem WithBot.not_coe_le_bot {α : Type u_1} [LE α] (a : α) :
            @[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 α} :
            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} [LE α] {a : α} {b : WithBot α} (h : b ) :
            theorem WithBot.unbot_le_iff {α : Type u_1} [LE α] {a : WithBot α} (h : a ) {b : α} :
            a.unbot h b a b
            theorem WithBot.unbot'_le_iff {α : Type u_1} [LE α] {a : WithBot α} {b c : α} (h : a = b c) :
            unbot' b a c a c
            @[instance 10]
            instance WithBot.lt {α : Type u_1} [LT α] :
            LT (WithBot α)
            Equations
            @[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 α) :
            @[simp, deprecated WithBot.coe_lt_coe "Don't mix Option and WithBot" (since := "2024-05-27")]
            theorem WithBot.some_lt_some {α : Type u_1} {a b : α} [LT α] :
            @[simp, deprecated WithBot.bot_lt_coe "Don't mix Option and WithBot" (since := "2024-05-27")]
            theorem WithBot.none_lt_some {α : Type u_1} [LT α] (a : α) :
            none < a
            @[simp, deprecated not_lt_bot "Don't mix Option and WithBot" (since := "2024-05-27")]
            theorem WithBot.not_lt_none {α : Type u_1} [LT α] (a : WithBot α) :
            theorem WithBot.lt_iff_exists_coe {α : Type u_1} [LT α] {a b : WithBot α} :
            a < b (p : α), b = p a < p
            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} [LT α] {a : α} {b : WithBot α} (h : b ) :
            theorem WithBot.unbot_lt_iff {α : Type u_1} [LT α] {a : WithBot α} (h : a ) {b : α} :
            a.unbot h < b a < b
            theorem WithBot.unbot'_lt_iff {α : Type u_1} [LT α] {a : WithBot α} {b c : α} (h : a = b < c) :
            unbot' b a < c a < c
            instance WithBot.preorder {α : Type u_1} [Preorder α] :
            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 β] (f : αβ) (mono_iff : ∀ {a b : α}, f a f b a b) (a b : WithBot α) :
            map f a map f b a b
            theorem WithBot.le_coe_unbot' {α : Type u_1} [Preorder α] (a : WithBot α) (b : α) :
            a (unbot' b a)
            @[simp]
            theorem WithBot.lt_coe_bot {α : Type u_1} [Preorder α] [OrderBot α] {x : WithBot α} :
            Equations
            • One or more equations did not get rendered due to their size.
            theorem WithBot.coe_sup {α : Type u_1} [SemilatticeSup α] (a b : α) :
            Equations
            theorem WithBot.coe_inf {α : Type u_1} [SemilatticeInf α] (a b : α) :
            instance WithBot.decidableLE {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 x2] :
            DecidableRel fun (x1 x2 : WithBot α) => x1 x2
            Equations
            instance WithBot.decidableLT {α : Type u_1} [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] :
            DecidableRel fun (x1 x2 : WithBot α) => x1 < x2
            Equations
            instance WithBot.isTotal_le {α : Type u_1} [LE α] [IsTotal α fun (x1 x2 : α) => x1 x2] :
            IsTotal (WithBot α) fun (x1 x2 : WithBot α) => x1 x2
            @[simp]
            theorem WithBot.coe_min {α : Type u_1} [LinearOrder α] (x y : α) :
            @[simp]
            theorem WithBot.coe_max {α : Type u_1} [LinearOrder α] (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 : α} :

            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]
                    def WithTop.untop' {α : Type u_1} (d : α) (x : WithTop α) :
                    α

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

                    Equations
                    Instances For
                      @[simp]
                      theorem WithTop.untop'_top {α : Type u_5} (d : α) :
                      @[simp]
                      theorem WithTop.untop'_coe {α : Type u_5} (d x : α) :
                      untop' d x = x
                      @[simp]
                      theorem WithTop.coe_eq_coe {α : Type u_1} {a b : α} :
                      a = b a = b
                      theorem WithTop.untop'_eq_iff {α : Type u_1} {d y : α} {x : WithTop α} :
                      untop' d x = y x = y x = y = d
                      @[simp]
                      theorem WithTop.untop'_eq_self_iff {α : Type u_1} {d : α} {x : WithTop α} :
                      untop' d x = d x = d x =
                      theorem WithTop.untop'_eq_untop'_iff {α : Type u_1} {d : α} {x y : WithTop α} :
                      untop' d x = untop' d y x = y x = d y = x = y = d
                      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 α} :
                        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 β} :
                          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.ne_top_iff_exists {α : Type u_1} {x : WithTop α} :
                          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 ) :
                            @[simp]
                            theorem WithTop.untop_coe {α : Type u_1} (x : α) (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 : α} :
                            @[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 ) :
                            def Equiv.withTopSubtypeNe {α : Type u_1} :

                            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]
                              @[instance 10]
                              instance WithTop.le {α : Type u_1} [LE α] :
                              LE (WithTop α)
                              Equations
                              @[simp]
                              @[simp]
                              theorem WithTop.coe_le_coe {α : Type u_1} {a b : α} [LE α] :
                              @[simp, deprecated WithTop.coe_le_coe "Don't mix Option and WithTop" (since := "2024-05-27")]
                              theorem WithTop.some_le_some {α : Type u_1} {a b : α} [LE α] :
                              instance WithTop.orderTop {α : Type u_1} [LE α] :
                              Equations
                              @[simp, deprecated le_top "Don't mix Option and WithTop" (since := "2024-05-27")]
                              theorem WithTop.le_none {α : Type u_1} [LE α] {a : WithTop α} :
                              instance WithTop.orderBot {α : Type u_1} [LE α] [OrderBot α] :
                              Equations
                              theorem WithTop.not_top_le_coe {α : Type u_1} [LE α] (a : α) :
                              ¬ a
                              @[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} [LE α] {a : WithTop α} {b : α} (h : a ) :
                              a.untop h b a b
                              theorem WithTop.le_untop_iff {α : Type u_1} [LE α] {a : α} {b : WithTop α} (h : b ) :
                              theorem WithTop.le_untop'_iff {α : Type u_1} [LE α] {a : WithTop α} {b c : α} (h : a = c b) :
                              @[instance 10]
                              instance WithTop.lt {α : Type u_1} [LT α] :
                              LT (WithTop α)
                              Equations
                              @[simp]
                              theorem WithTop.lt_untop_iff {α : Type u_1} [LT α] {a : α} {b : WithTop α} (h : b ) :
                              theorem WithTop.untop_lt_iff {α : Type u_1} [LT α] {a : WithTop α} {b : α} (h : a ) :
                              a.untop h < b a < b
                              theorem WithTop.lt_untop'_iff {α : Type u_1} [LT α] {a : WithTop α} {b c : α} (h : a = c < b) :
                              @[simp]
                              theorem WithBot.toDual_apply_coe {α : Type u_1} (a : α) :
                              @[simp]
                              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 α) :
                              @[simp]
                              @[simp]
                              @[simp]
                              theorem WithTop.coe_lt_coe {α : Type u_1} [LT α] {a b : α} :
                              a < b a < b
                              @[simp]
                              theorem WithTop.coe_lt_top {α : Type u_1} [LT α] (a : α) :
                              @[simp]
                              theorem WithTop.not_top_lt {α : Type u_1} [LT α] (a : WithTop α) :
                              @[simp, deprecated WithTop.coe_lt_coe "Don't mix Option and WithTop" (since := "2024-05-27")]
                              theorem WithTop.some_lt_some {α : Type u_1} [LT α] {a b : α} :
                              @[simp, deprecated WithTop.coe_lt_top "Don't mix Option and WithTop" (since := "2024-05-27")]
                              theorem WithTop.some_lt_none {α : Type u_1} [LT α] (a : α) :
                              @[simp, deprecated not_top_lt "Don't mix Option and WithTop" (since := "2024-05-27")]
                              theorem WithTop.not_none_lt {α : Type u_1} [LT α] (a : WithTop α) :
                              theorem WithTop.lt_iff_exists_coe {α : Type u_1} [LT α] {a b : WithTop α} :
                              a < b (p : α), a = p p < b
                              theorem WithTop.coe_lt_iff {α : Type u_1} [LT α] {a : α} {x : WithTop α} :
                              a < x ∀ (b : α), x = 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 α.

                              instance WithTop.preorder {α : Type u_1} [Preorder α] :
                              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 β] (f : αβ) (a b : WithTop α) (mono_iff : ∀ {a b : α}, f a f b a b) :
                              map f a map f b a b
                              theorem WithTop.coe_untop'_le {α : Type u_1} [Preorder α] (a : WithTop α) (b : α) :
                              @[simp]
                              theorem WithTop.coe_top_lt {α : Type u_1} [Preorder α] [OrderTop α] {x : WithTop α} :
                              theorem WithTop.coe_inf {α : Type u_1} [SemilatticeInf α] (a b : α) :
                              Equations
                              theorem WithTop.coe_sup {α : Type u_1} [SemilatticeSup α] (a b : α) :
                              instance WithTop.decidableLE {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 x2] :
                              DecidableRel fun (x1 x2 : WithTop α) => x1 x2
                              Equations
                              instance WithTop.decidableLT {α : Type u_1} [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] :
                              DecidableRel fun (x1 x2 : WithTop α) => x1 < x2
                              Equations
                              instance WithTop.isTotal_le {α : Type u_1} [LE α] [IsTotal α fun (x1 x2 : α) => x1 x2] :
                              IsTotal (WithTop α) fun (x1 x2 : WithTop α) => x1 x2
                              @[simp]
                              theorem WithTop.coe_min {α : Type u_1} [LinearOrder α] (x y : α) :
                              @[simp]
                              theorem WithTop.coe_max {α : Type u_1} [LinearOrder α] (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 α] :