Documentation

Mathlib.Order.WithBot

WithBot, WithTop #

Adding a bot or a top to an order.

Main declarations #

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.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
        theorem WithBot.forall_ne_iff_eq_bot {α : Type u_1} {x : WithBot α} :
        (∀ (a : α), a x) 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 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
          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
          @[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.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.lt_unbot_iff {α : Type u_1} [LT α] {a : α} {b : WithBot α} (h : b ) :
          a < b.unbot h a < 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) :
          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
          • =
          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

          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
                        theorem WithTop.forall_ne_iff_eq_top {α : Type u_1} {x : WithTop α} :
                        (∀ (a : α), a x) 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 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
                          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
                          @[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.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 : α} {b : WithTop α} (h : b ) :
                          a < b.untop h a < 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) :
                          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.forall_lt_iff_eq_bot {α : Type u_1} [Preorder α] {x : WithBot α} :
                          (∀ (y : α), x < y) x =
                          theorem WithBot.forall_le_iff_eq_bot {α : Type u_1} [Preorder α] [NoMinOrder α] {x : WithBot α} :
                          (∀ (y : α), x y) x =
                          theorem WithBot.le_of_forall_lt_iff_le {α : Type u_1} [LinearOrder α] [DenselyOrdered α] [NoMinOrder α] {x : WithBot α} {y : WithBot α} :
                          (∀ (z : α), x < zy z) y x
                          theorem WithBot.ge_of_forall_gt_iff_ge {α : Type u_1} [LinearOrder α] [DenselyOrdered α] [NoMinOrder α] {x : WithBot α} {y : WithBot α} :
                          (∀ (z : α), z < xz y) x y
                          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 =
                          theorem WithTop.forall_gt_iff_eq_top {α : Type u_1} [Preorder α] {x : WithTop α} :
                          (∀ (y : α), y < x) x =
                          theorem WithTop.forall_ge_iff_eq_top {α : Type u_1} [Preorder α] [NoMaxOrder α] {x : WithTop α} :
                          (∀ (y : α), y x) x =
                          theorem WithTop.le_of_forall_lt_iff_le {α : Type u_1} [LinearOrder α] [DenselyOrdered α] [NoMaxOrder α] {x : WithTop α} {y : WithTop α} :
                          (∀ (z : α), x < zy z) y x
                          theorem WithTop.ge_of_forall_gt_iff_ge {α : Type u_1} [LinearOrder α] [DenselyOrdered α] [NoMaxOrder α] {x : WithTop α} {y : WithTop α} :
                          (∀ (z : α), z < xz y) x y
                          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
                          • =