Documentation

Mathlib.Order.WithBot

WithBot, WithTop #

Adding a bot or a top to an order.

Main declarations #

def WithBot (α : Type u_5) :
Type u_5

Attach to a type.

Equations
Instances For
    instance WithBot.instRepr {α : Type u_1} [Repr α] :
    Equations
    @[match_pattern]
    def WithBot.some {α : Type u_1} :
    αWithBot α

    The canonical map from α into WithBot α

    Equations
    • WithBot.some = some
    Instances For
      instance WithBot.coe {α : Type u_1} :
      Coe α (WithBot α)
      Equations
      • WithBot.coe = { coe := WithBot.some }
      instance WithBot.bot {α : Type u_1} :
      Equations
      • WithBot.bot = { bot := none }
      instance WithBot.inhabited {α : Type u_1} :
      Equations
      • WithBot.inhabited = { default := }
      instance WithBot.nontrivial {α : Type u_1} [Nonempty α] :
      Equations
      • =
      theorem WithBot.coe_injective {α : Type u_1} :
      Function.Injective WithBot.some
      @[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.none_eq_bot {α : Type u_1} :
      none =
      theorem WithBot.some_eq_coe {α : Type u_1} (a : α) :
      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.recBotCoe {α : Type u_1} {C : WithBot αSort u_5} (bot : C ) (coe : (a : α) → C a) (n : WithBot α) :
      C n

      Recursor for WithBot using the preferred forms and ↑a.

      Equations
      Instances For
        @[simp]
        theorem WithBot.recBotCoe_bot {α : Type u_1} {C : WithBot αSort u_5} (d : C ) (f : (a : α) → C a) :
        @[simp]
        theorem WithBot.recBotCoe_coe {α : Type u_1} {C : WithBot αSort u_5} (d : C ) (f : (a : α) → C a) (x : α) :
        WithBot.recBotCoe d f x = f x
        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 : α) :
          WithBot.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 α} :
          WithBot.unbot' d x = y x = y x = y = d
          @[simp]
          theorem WithBot.unbot'_eq_self_iff {α : Type u_1} {d : α} {x : WithBot α} :
          WithBot.unbot' d x = d x = d x =
          theorem WithBot.unbot'_eq_unbot'_iff {α : Type u_1} {d : α} {x : WithBot α} {y : WithBot α} :
          WithBot.unbot' d x = WithBot.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 : α) :
            WithBot.map f a = (f a)
            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 : α) :
            WithBot.map g₁ (WithBot.map f₁ a) = WithBot.map g₂ (WithBot.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
            • WithBot.map₂ = Option.map₂
            Instances For
              theorem WithBot.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : β) :
              WithBot.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 β) :
              WithBot.map₂ f (a) b = WithBot.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 : β) :
              WithBot.map₂ f a b = WithBot.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 α} :
              x ∃ (a : α), a = x
              def WithBot.unbot {α : Type u_1} (x : WithBot α) :
              x α

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

              Equations
              • x✝.unbot x = match x✝, x with | some x, x_1 => x
              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 : optParam (x ) ) :
                (x).unbot h = x
                instance WithBot.canLift {α : Type u_1} :
                CanLift (WithBot α) α WithBot.some fun (r : WithBot α) => r
                Equations
                • =
                @[instance 10]
                instance WithBot.le {α : Type u_1} [LE α] :
                LE (WithBot α)
                Equations
                • WithBot.le = { le := fun (o₁ o₂ : WithBot α) => ∀ (a : α), o₁ = a∃ (b : α), o₂ = b a b }
                @[simp]
                theorem WithBot.coe_le_coe {α : Type u_1} {a : α} {b : α} [LE α] :
                a b a b
                instance WithBot.orderBot {α : Type u_1} [LE α] :
                Equations
                @[simp, deprecated WithBot.coe_le_coe]
                theorem WithBot.some_le_some {α : Type u_1} {a : α} {b : α} [LE α] :
                some a some b a b
                @[simp, deprecated bot_le]
                theorem WithBot.none_le {α : Type u_1} [LE α] {a : WithBot α} :
                none a
                instance WithBot.instTop {α : Type u_1} [Top α] :
                Equations
                • WithBot.instTop = { top := }
                @[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
                instance WithBot.orderTop {α : Type u_1} [LE α] [OrderTop α] :
                Equations
                instance WithBot.instBoundedOrder {α : Type u_1} [LE α] [OrderTop α] :
                Equations
                • WithBot.instBoundedOrder = let __src := WithBot.orderBot; let __src_1 := WithBot.orderTop; BoundedOrder.mk
                theorem WithBot.not_coe_le_bot {α : Type u_1} [LE α] (a : α) :
                ¬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 α} :
                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} [LE α] {a : α} {b : WithBot α} (h : b ) :
                a b.unbot h a 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) :
                WithBot.unbot' b a c a c
                @[instance 10]
                instance WithBot.lt {α : Type u_1} [LT α] :
                LT (WithBot α)
                Equations
                • WithBot.lt = { lt := fun (o₁ o₂ : WithBot α) => ∃ (b : α), o₂ = b ∀ (a : α), o₁ = 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 α) :
                @[simp, deprecated WithBot.coe_lt_coe]
                theorem WithBot.some_lt_some {α : Type u_1} {a : α} {b : α} [LT α] :
                some a < some b a < b
                @[simp, deprecated WithBot.bot_lt_coe]
                theorem WithBot.none_lt_some {α : Type u_1} [LT α] (a : α) :
                none < a
                @[simp, deprecated not_lt_bot]
                theorem WithBot.not_lt_none {α : Type u_1} [LT α] (a : WithBot α) :
                ¬a < none
                theorem WithBot.lt_iff_exists_coe {α : Type u_1} [LT α] {a : WithBot α} {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.unbot'_lt_iff {α : Type u_1} [LT α] {a : WithBot α} {b : α} {c : α} (h : a = b < c) :
                WithBot.unbot' b a < c a < c
                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 β] (f : αβ) (mono_iff : ∀ {a b : α}, f a f b a b) (a : WithBot α) (b : WithBot α) :
                theorem WithBot.le_coe_unbot' {α : Type u_1} [Preorder α] (a : WithBot α) (b : α) :
                a (WithBot.unbot' b a)
                @[simp]
                theorem WithBot.lt_coe_bot {α : Type u_1} [Preorder α] [OrderBot α] {x : WithBot α} :
                x < x =
                Equations
                theorem WithBot.coe_sup {α : Type u_1} [SemilatticeSup α] (a : α) (b : α) :
                (a b) = a b
                Equations
                • WithBot.semilatticeInf = let __src := WithBot.partialOrder; let __src_1 := WithBot.orderBot; SemilatticeInf.mk
                theorem WithBot.coe_inf {α : Type u_1} [SemilatticeInf α] (a : α) (b : α) :
                (a b) = a b
                instance WithBot.lattice {α : Type u_1} [Lattice α] :
                Equations
                • WithBot.lattice = let __src := WithBot.semilatticeSup; let __src_1 := WithBot.semilatticeInf; Lattice.mk
                Equations
                instance WithBot.decidableEq {α : Type u_1} [DecidableEq α] :
                Equations
                instance WithBot.decidableLE {α : Type u_1} [LE α] [DecidableRel fun (x x_1 : α) => x x_1] :
                DecidableRel fun (x x_1 : WithBot α) => x x_1
                Equations
                instance WithBot.decidableLT {α : Type u_1} [LT α] [DecidableRel fun (x x_1 : α) => x < x_1] :
                DecidableRel fun (x x_1 : WithBot α) => x < x_1
                Equations
                instance WithBot.isTotal_le {α : Type u_1} [LE α] [IsTotal α fun (x x_1 : α) => x x_1] :
                IsTotal (WithBot α) fun (x x_1 : WithBot α) => x x_1
                Equations
                • =
                instance WithBot.linearOrder {α : Type u_1} [LinearOrder α] :
                Equations
                @[simp]
                theorem WithBot.coe_min {α : Type u_1} [LinearOrder α] (x : α) (y : α) :
                (min x y) = min x y
                @[simp]
                theorem WithBot.coe_max {α : Type u_1} [LinearOrder α] (x : α) (y : α) :
                (max x y) = max x y
                Equations
                • =
                Equations
                • =
                Equations
                • =
                theorem WithBot.lt_iff_exists_coe_btwn {α : Type u_1} [Preorder α] [DenselyOrdered α] [NoMinOrder α] {a : WithBot α} {b : WithBot α} :
                a < b ∃ (x : α), a < x x < b
                instance WithBot.noTopOrder {α : Type u_1} [LE α] [NoTopOrder α] [Nonempty α] :
                Equations
                • =
                instance WithBot.noMaxOrder {α : Type u_1} [LT α] [NoMaxOrder α] [Nonempty α] :
                Equations
                • =
                def WithTop (α : Type u_5) :
                Type u_5

                Attach to a type.

                Equations
                Instances For
                  instance WithTop.instRepr {α : Type u_1} [Repr α] :
                  Equations
                  @[match_pattern]
                  def WithTop.some {α : Type u_1} :
                  αWithTop α

                  The canonical map from α into WithTop α

                  Equations
                  • WithTop.some = some
                  Instances For
                    instance WithTop.coeTC {α : Type u_1} :
                    CoeTC α (WithTop α)
                    Equations
                    • WithTop.coeTC = { coe := WithTop.some }
                    instance WithTop.top {α : Type u_1} :
                    Equations
                    • WithTop.top = { top := none }
                    instance WithTop.inhabited {α : Type u_1} :
                    Equations
                    • WithTop.inhabited = { default := }
                    instance WithTop.nontrivial {α : Type u_1} [Nonempty α] :
                    Equations
                    • =
                    theorem WithTop.coe_injective {α : Type u_1} :
                    Function.Injective WithTop.some
                    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.none_eq_top {α : Type u_1} :
                    none =
                    theorem WithTop.some_eq_coe {α : Type u_1} (a : α) :
                    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
                    def WithTop.recTopCoe {α : Type u_1} {C : WithTop αSort u_5} (top : C ) (coe : (a : α) → C a) (n : WithTop α) :
                    C n

                    Recursor for WithTop using the preferred forms and ↑a.

                    Equations
                    Instances For
                      @[simp]
                      theorem WithTop.recTopCoe_top {α : Type u_1} {C : WithTop αSort u_5} (d : C ) (f : (a : α) → C a) :
                      @[simp]
                      theorem WithTop.recTopCoe_coe {α : Type u_1} {C : WithTop αSort u_5} (d : C ) (f : (a : α) → C a) (x : α) :
                      WithTop.recTopCoe d f x = f x

                      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_symm_apply {α : Type u_1} (a : WithBot αᵒᵈ) :
                              WithTop.toDual.symm a = WithBot.ofDual a
                              @[simp]
                              theorem WithTop.ofDual_symm_apply {α : Type u_1} (a : WithBot α) :
                              WithTop.ofDual.symm a = WithBot.toDual a
                              @[simp]
                              theorem WithTop.toDual_apply_top {α : Type u_1} :
                              WithTop.toDual =
                              @[simp]
                              theorem WithTop.ofDual_apply_top {α : Type u_1} :
                              WithTop.ofDual =
                              @[simp]
                              theorem WithTop.toDual_apply_coe {α : Type u_1} (a : α) :
                              WithTop.toDual a = (OrderDual.toDual a)
                              @[simp]
                              theorem WithTop.ofDual_apply_coe {α : Type u_1} (a : αᵒᵈ) :
                              WithTop.ofDual a = (OrderDual.ofDual a)
                              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 : α) :
                                WithTop.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 α} :
                                WithTop.untop' d x = y x = y x = y = d
                                @[simp]
                                theorem WithTop.untop'_eq_self_iff {α : Type u_1} {d : α} {x : WithTop α} :
                                WithTop.untop' d x = d x = d x =
                                theorem WithTop.untop'_eq_untop'_iff {α : Type u_1} {d : α} {x : WithTop α} {y : WithTop α} :
                                WithTop.untop' d x = WithTop.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 : α) :
                                  WithTop.map f a = (f a)
                                  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 : α) :
                                  WithTop.map g₁ (WithTop.map f₁ a) = WithTop.map g₂ (WithTop.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
                                  • WithTop.map₂ = Option.map₂
                                  Instances For
                                    theorem WithTop.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : β) :
                                    WithTop.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 β) :
                                    WithTop.map₂ f (a) b = WithTop.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 : β) :
                                    WithTop.map₂ f a b = WithTop.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 α) :
                                    WithTop.map f (WithBot.toDual a) = WithBot.map (OrderDual.toDual f) a
                                    theorem WithTop.map_ofDual {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithBot αᵒᵈ) :
                                    WithTop.map f (WithBot.ofDual a) = WithBot.map (OrderDual.ofDual f) a
                                    theorem WithTop.toDual_map {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithTop α) :
                                    WithTop.toDual (WithTop.map f a) = WithBot.map (OrderDual.toDual f OrderDual.ofDual) (WithTop.toDual a)
                                    theorem WithTop.ofDual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : WithTop αᵒᵈ) :
                                    WithTop.ofDual (WithTop.map f a) = WithBot.map (OrderDual.ofDual f OrderDual.toDual) (WithTop.ofDual a)
                                    theorem WithTop.ne_top_iff_exists {α : Type u_1} {x : WithTop α} :
                                    x ∃ (a : α), a = x
                                    def WithTop.untop {α : Type u_1} (x : WithTop α) :
                                    x α

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

                                    Equations
                                    • x✝.untop x = match x✝, x with | some x, x_1 => x
                                    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 : optParam (x ) ) :
                                      (x).untop h = x
                                      instance WithTop.canLift {α : Type u_1} :
                                      CanLift (WithTop α) α WithTop.some fun (r : WithTop α) => r
                                      Equations
                                      • =
                                      @[instance 10]
                                      instance WithTop.le {α : Type u_1} [LE α] :
                                      LE (WithTop α)
                                      Equations
                                      • WithTop.le = { le := fun (o₁ o₂ : WithTop α) => ∀ (a : α), o₂ = a∃ (b : α), o₁ = b b a }
                                      theorem WithTop.toDual_le_iff {α : Type u_1} [LE α] {a : WithTop α} {b : WithBot αᵒᵈ} :
                                      WithTop.toDual a b WithBot.ofDual b a
                                      theorem WithTop.le_toDual_iff {α : Type u_1} [LE α] {a : WithBot αᵒᵈ} {b : WithTop α} :
                                      a WithTop.toDual b b WithBot.ofDual a
                                      @[simp]
                                      theorem WithTop.toDual_le_toDual_iff {α : Type u_1} [LE α] {a : WithTop α} {b : WithTop α} :
                                      WithTop.toDual a WithTop.toDual b b a
                                      theorem WithTop.ofDual_le_iff {α : Type u_1} [LE α] {a : WithTop αᵒᵈ} {b : WithBot α} :
                                      WithTop.ofDual a b WithBot.toDual b a
                                      theorem WithTop.le_ofDual_iff {α : Type u_1} [LE α] {a : WithBot α} {b : WithTop αᵒᵈ} :
                                      a WithTop.ofDual b b WithBot.toDual a
                                      @[simp]
                                      theorem WithTop.ofDual_le_ofDual_iff {α : Type u_1} [LE α] {a : WithTop αᵒᵈ} {b : WithTop αᵒᵈ} :
                                      WithTop.ofDual a WithTop.ofDual b b a
                                      @[simp]
                                      theorem WithTop.coe_le_coe {α : Type u_1} {a : α} {b : α} [LE α] :
                                      a b a b
                                      @[simp, deprecated WithTop.coe_le_coe]
                                      theorem WithTop.some_le_some {α : Type u_1} {a : α} {b : α} [LE α] :
                                      some a some b a b
                                      instance WithTop.orderTop {α : Type u_1} [LE α] :
                                      Equations
                                      @[simp, deprecated le_top]
                                      theorem WithTop.le_none {α : Type u_1} [LE α] {a : WithTop α} :
                                      a none
                                      instance WithTop.instBot {α : Type u_1} [Bot α] :
                                      Equations
                                      • WithTop.instBot = { bot := }
                                      @[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
                                      instance WithTop.orderBot {α : Type u_1} [LE α] [OrderBot α] :
                                      Equations
                                      instance WithTop.boundedOrder {α : Type u_1} [LE α] [OrderBot α] :
                                      Equations
                                      • WithTop.boundedOrder = let __src := WithTop.orderTop; let __src_1 := WithTop.orderBot; BoundedOrder.mk
                                      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 ) :
                                      a b.untop h a b
                                      theorem WithTop.le_untop'_iff {α : Type u_1} [LE α] {a : WithTop α} {b : α} {c : α} (h : a = c b) :
                                      c WithTop.untop' b a c a
                                      @[instance 10]
                                      instance WithTop.lt {α : Type u_1} [LT α] :
                                      LT (WithTop α)
                                      Equations
                                      • WithTop.lt = { lt := fun (o₁ o₂ : Option α) => ∃ (b : α), b o₁ ∀ (a : α), a o₂b < a }
                                      theorem WithTop.toDual_lt_iff {α : Type u_1} [LT α] {a : WithTop α} {b : WithBot αᵒᵈ} :
                                      WithTop.toDual a < b WithBot.ofDual b < a
                                      theorem WithTop.lt_toDual_iff {α : Type u_1} [LT α] {a : WithBot αᵒᵈ} {b : WithTop α} :
                                      a < WithTop.toDual b b < WithBot.ofDual a
                                      @[simp]
                                      theorem WithTop.toDual_lt_toDual_iff {α : Type u_1} [LT α] {a : WithTop α} {b : WithTop α} :
                                      WithTop.toDual a < WithTop.toDual b b < a
                                      theorem WithTop.ofDual_lt_iff {α : Type u_1} [LT α] {a : WithTop αᵒᵈ} {b : WithBot α} :
                                      WithTop.ofDual a < b WithBot.toDual b < a
                                      theorem WithTop.lt_ofDual_iff {α : Type u_1} [LT α] {a : WithBot α} {b : WithTop αᵒᵈ} :
                                      a < WithTop.ofDual b b < WithBot.toDual a
                                      @[simp]
                                      theorem WithTop.ofDual_lt_ofDual_iff {α : Type u_1} [LT α] {a : WithTop αᵒᵈ} {b : WithTop αᵒᵈ} :
                                      WithTop.ofDual a < WithTop.ofDual b b < a
                                      theorem WithTop.lt_untop'_iff {α : Type u_1} [LT α] {a : WithTop α} {b : α} {c : α} (h : a = c < b) :
                                      c < WithTop.untop' b a c < a
                                      @[simp]
                                      theorem WithBot.toDual_symm_apply {α : Type u_1} (a : WithTop αᵒᵈ) :
                                      WithBot.toDual.symm a = WithTop.ofDual a
                                      @[simp]
                                      theorem WithBot.ofDual_symm_apply {α : Type u_1} (a : WithTop α) :
                                      WithBot.ofDual.symm a = WithTop.toDual a
                                      @[simp]
                                      theorem WithBot.toDual_apply_bot {α : Type u_1} :
                                      WithBot.toDual =
                                      @[simp]
                                      theorem WithBot.ofDual_apply_bot {α : Type u_1} :
                                      WithBot.ofDual =
                                      @[simp]
                                      theorem WithBot.toDual_apply_coe {α : Type u_1} (a : α) :
                                      WithBot.toDual a = (OrderDual.toDual a)
                                      @[simp]
                                      theorem WithBot.ofDual_apply_coe {α : Type u_1} (a : αᵒᵈ) :
                                      WithBot.ofDual a = (OrderDual.ofDual a)
                                      theorem WithBot.map_toDual {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : WithTop α) :
                                      WithBot.map f (WithTop.toDual a) = WithTop.map (OrderDual.toDual f) a
                                      theorem WithBot.map_ofDual {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithTop αᵒᵈ) :
                                      WithBot.map f (WithTop.ofDual a) = WithTop.map (OrderDual.ofDual f) a
                                      theorem WithBot.toDual_map {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithBot α) :
                                      WithBot.toDual (WithBot.map f a) = WithBot.map (OrderDual.toDual f OrderDual.ofDual) (WithBot.toDual a)
                                      theorem WithBot.ofDual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : WithBot αᵒᵈ) :
                                      WithBot.ofDual (WithBot.map f a) = WithBot.map (OrderDual.ofDual f OrderDual.toDual) (WithBot.ofDual a)
                                      theorem WithBot.toDual_le_iff {α : Type u_1} [LE α] {a : WithBot α} {b : WithTop αᵒᵈ} :
                                      WithBot.toDual a b WithTop.ofDual b a
                                      theorem WithBot.le_toDual_iff {α : Type u_1} [LE α] {a : WithTop αᵒᵈ} {b : WithBot α} :
                                      a WithBot.toDual b b WithTop.ofDual a
                                      @[simp]
                                      theorem WithBot.toDual_le_toDual_iff {α : Type u_1} [LE α] {a : WithBot α} {b : WithBot α} :
                                      WithBot.toDual a WithBot.toDual b b a
                                      theorem WithBot.ofDual_le_iff {α : Type u_1} [LE α] {a : WithBot αᵒᵈ} {b : WithTop α} :
                                      WithBot.ofDual a b WithTop.toDual b a
                                      theorem WithBot.le_ofDual_iff {α : Type u_1} [LE α] {a : WithTop α} {b : WithBot αᵒᵈ} :
                                      a WithBot.ofDual b b WithTop.toDual a
                                      @[simp]
                                      theorem WithBot.ofDual_le_ofDual_iff {α : Type u_1} [LE α] {a : WithBot αᵒᵈ} {b : WithBot αᵒᵈ} :
                                      WithBot.ofDual a WithBot.ofDual b b a
                                      theorem WithBot.toDual_lt_iff {α : Type u_1} [LT α] {a : WithBot α} {b : WithTop αᵒᵈ} :
                                      WithBot.toDual a < b WithTop.ofDual b < a
                                      theorem WithBot.lt_toDual_iff {α : Type u_1} [LT α] {a : WithTop αᵒᵈ} {b : WithBot α} :
                                      a < WithBot.toDual b b < WithTop.ofDual a
                                      @[simp]
                                      theorem WithBot.toDual_lt_toDual_iff {α : Type u_1} [LT α] {a : WithBot α} {b : WithBot α} :
                                      WithBot.toDual a < WithBot.toDual b b < a
                                      theorem WithBot.ofDual_lt_iff {α : Type u_1} [LT α] {a : WithBot αᵒᵈ} {b : WithTop α} :
                                      WithBot.ofDual a < b WithTop.toDual b < a
                                      theorem WithBot.lt_ofDual_iff {α : Type u_1} [LT α] {a : WithTop α} {b : WithBot αᵒᵈ} :
                                      a < WithBot.ofDual b b < WithTop.toDual a
                                      @[simp]
                                      theorem WithBot.ofDual_lt_ofDual_iff {α : Type u_1} [LT α] {a : WithBot αᵒᵈ} {b : WithBot αᵒᵈ} :
                                      WithBot.ofDual a < WithBot.ofDual b b < a
                                      @[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 : α) :
                                      a <
                                      @[simp]
                                      theorem WithTop.not_top_lt {α : Type u_1} [LT α] (a : WithTop α) :
                                      @[simp, deprecated WithTop.coe_lt_coe]
                                      theorem WithTop.some_lt_some {α : Type u_1} [LT α] {a : α} {b : α} :
                                      some a < some b a < b
                                      @[simp, deprecated WithTop.coe_lt_top]
                                      theorem WithTop.some_lt_none {α : Type u_1} [LT α] (a : α) :
                                      some a < none
                                      @[simp, deprecated not_top_lt]
                                      theorem WithTop.not_none_lt {α : Type u_1} [LT α] (a : WithTop α) :
                                      ¬none < a
                                      theorem WithTop.lt_iff_exists_coe {α : Type u_1} [LT α] {a : WithTop α} {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
                                      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 : WithTop α) (b : WithTop α) (mono_iff : ∀ {a b : α}, f a f b a b) :
                                      theorem WithTop.coe_untop'_le {α : Type u_1} [Preorder α] (a : WithTop α) (b : α) :
                                      (WithTop.untop' b a) a
                                      @[simp]
                                      theorem WithTop.coe_top_lt {α : Type u_1} [Preorder α] [OrderTop α] {x : WithTop α} :
                                      < x x =
                                      Equations
                                      theorem WithTop.coe_inf {α : Type u_1} [SemilatticeInf α] (a : α) (b : α) :
                                      (a b) = a b
                                      Equations
                                      theorem WithTop.coe_sup {α : Type u_1} [SemilatticeSup α] (a : α) (b : α) :
                                      (a b) = a b
                                      instance WithTop.lattice {α : Type u_1} [Lattice α] :
                                      Equations
                                      • WithTop.lattice = let __src := WithTop.semilatticeSup; let __src_1 := WithTop.semilatticeInf; Lattice.mk
                                      Equations
                                      instance WithTop.decidableEq {α : Type u_1} [DecidableEq α] :
                                      Equations
                                      instance WithTop.decidableLE {α : Type u_1} [LE α] [DecidableRel fun (x x_1 : α) => x x_1] :
                                      DecidableRel fun (x x_1 : WithTop α) => x x_1
                                      Equations
                                      instance WithTop.decidableLT {α : Type u_1} [LT α] [DecidableRel fun (x x_1 : α) => x < x_1] :
                                      DecidableRel fun (x x_1 : WithTop α) => x < x_1
                                      Equations
                                      instance WithTop.isTotal_le {α : Type u_1} [LE α] [IsTotal α fun (x x_1 : α) => x x_1] :
                                      IsTotal (WithTop α) fun (x x_1 : WithTop α) => x x_1
                                      Equations
                                      • =
                                      instance WithTop.linearOrder {α : Type u_1} [LinearOrder α] :
                                      Equations
                                      @[simp]
                                      theorem WithTop.coe_min {α : Type u_1} [LinearOrder α] (x : α) (y : α) :
                                      (min x y) = min x y
                                      @[simp]
                                      theorem WithTop.coe_max {α : Type u_1} [LinearOrder α] (x : α) (y : α) :
                                      (max x y) = max x y
                                      Equations
                                      • =
                                      Equations
                                      • =
                                      instance WithTop.trichotomous.lt {α : Type u_1} [Preorder α] [IsTrichotomous α fun (x x_1 : α) => x < x_1] :
                                      IsTrichotomous (WithTop α) fun (x x_1 : WithTop α) => x < x_1
                                      Equations
                                      • =
                                      instance WithTop.IsWellOrder.lt {α : Type u_1} [Preorder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] :
                                      IsWellOrder (WithTop α) fun (x x_1 : WithTop α) => x < x_1
                                      Equations
                                      • =
                                      instance WithTop.trichotomous.gt {α : Type u_1} [Preorder α] [IsTrichotomous α fun (x x_1 : α) => x > x_1] :
                                      IsTrichotomous (WithTop α) fun (x x_1 : WithTop α) => x > x_1
                                      Equations
                                      • =
                                      instance WithTop.IsWellOrder.gt {α : Type u_1} [Preorder α] [IsWellOrder α fun (x x_1 : α) => x > x_1] :
                                      IsWellOrder (WithTop α) fun (x x_1 : WithTop α) => x > x_1
                                      Equations
                                      • =
                                      instance WithBot.trichotomous.lt {α : Type u_1} [Preorder α] [h : IsTrichotomous α fun (x x_1 : α) => x < x_1] :
                                      IsTrichotomous (WithBot α) fun (x x_1 : WithBot α) => x < x_1
                                      Equations
                                      • =
                                      instance WithBot.isWellOrder.lt {α : Type u_1} [Preorder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] :
                                      IsWellOrder (WithBot α) fun (x x_1 : WithBot α) => x < x_1
                                      Equations
                                      • =
                                      instance WithBot.trichotomous.gt {α : Type u_1} [Preorder α] [h : IsTrichotomous α fun (x x_1 : α) => x > x_1] :
                                      IsTrichotomous (WithBot α) fun (x x_1 : WithBot α) => x > x_1
                                      Equations
                                      • =
                                      instance WithBot.isWellOrder.gt {α : Type u_1} [Preorder α] [h : IsWellOrder α fun (x x_1 : α) => x > x_1] :
                                      IsWellOrder (WithBot α) fun (x x_1 : WithBot α) => x > x_1
                                      Equations
                                      • =
                                      Equations
                                      • =
                                      theorem WithTop.lt_iff_exists_coe_btwn {α : Type u_1} [Preorder α] [DenselyOrdered α] [NoMaxOrder α] {a : WithTop α} {b : WithTop α} :
                                      a < b ∃ (x : α), a < x x < b
                                      instance WithTop.noBotOrder {α : Type u_1} [LE α] [NoBotOrder α] [Nonempty α] :
                                      Equations
                                      • =
                                      instance WithTop.noMinOrder {α : Type u_1} [LT α] [NoMinOrder α] [Nonempty α] :
                                      Equations
                                      • =