Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Adjoining top/bottom elements to ordered monoids. #

instance WithTop.one {α : Type u} [One α] :
Equations
    instance WithTop.zero {α : Type u} [Zero α] :
    Equations
      @[simp]
      theorem WithTop.coe_one {α : Type u} [One α] :
      1 = 1
      @[simp]
      theorem WithTop.coe_zero {α : Type u} [Zero α] :
      0 = 0
      @[simp]
      theorem WithTop.coe_eq_one {α : Type u} [One α] {a : α} :
      a = 1 a = 1
      @[simp]
      theorem WithTop.coe_eq_zero {α : Type u} [Zero α] {a : α} :
      a = 0 a = 0
      @[simp]
      theorem WithTop.one_eq_coe {α : Type u} [One α] {a : α} :
      1 = a a = 1
      @[simp]
      theorem WithTop.zero_eq_coe {α : Type u} [Zero α] {a : α} :
      0 = a a = 0
      @[simp]
      theorem WithTop.top_ne_one {α : Type u} [One α] :
      @[simp]
      theorem WithTop.top_ne_zero {α : Type u} [Zero α] :
      @[simp]
      theorem WithTop.one_ne_top {α : Type u} [One α] :
      @[simp]
      theorem WithTop.zero_ne_top {α : Type u} [Zero α] :
      @[simp]
      theorem WithTop.untop_one {α : Type u} [One α] :
      untop 1 = 1
      @[simp]
      theorem WithTop.untop_zero {α : Type u} [Zero α] :
      untop 0 = 0
      @[simp]
      theorem WithTop.untopD_one {α : Type u} [One α] (d : α) :
      untopD d 1 = 1
      @[simp]
      theorem WithTop.untopD_zero {α : Type u} [Zero α] (d : α) :
      untopD d 0 = 0
      @[deprecated WithTop.untopD_zero (since := "2025-02-06")]
      theorem WithTop.untop_zero' {α : Type u} [Zero α] (d : α) :
      untopD d 0 = 0

      Alias of WithTop.untopD_zero.

      @[deprecated WithTop.untopD_one (since := "2025-02-06")]
      theorem WithTop.untop_one' {α : Type u} [One α] (d : α) :
      untopD d 1 = 1

      Alias of WithTop.untopD_one.

      @[simp]
      theorem WithTop.one_le_coe {α : Type u} [One α] [LE α] {a : α} :
      1 a 1 a
      @[simp]
      theorem WithTop.coe_nonneg {α : Type u} [Zero α] [LE α] {a : α} :
      0 a 0 a
      @[simp]
      theorem WithTop.coe_le_one {α : Type u} [One α] [LE α] {a : α} :
      a 1 a 1
      @[simp]
      theorem WithTop.coe_le_zero {α : Type u} [Zero α] [LE α] {a : α} :
      a 0 a 0
      @[simp]
      theorem WithTop.one_lt_coe {α : Type u} [One α] [LT α] {a : α} :
      1 < a 1 < a
      @[simp]
      theorem WithTop.coe_pos {α : Type u} [Zero α] [LT α] {a : α} :
      0 < a 0 < a
      @[simp]
      theorem WithTop.coe_lt_one {α : Type u} [One α] [LT α] {a : α} :
      a < 1 a < 1
      @[simp]
      theorem WithTop.coe_lt_zero {α : Type u} [Zero α] [LT α] {a : α} :
      a < 0 a < 0
      @[simp]
      theorem WithTop.map_one {α : Type u} [One α] {β : Type u_1} (f : αβ) :
      map f 1 = (f 1)
      @[simp]
      theorem WithTop.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : αβ) :
      map f 0 = (f 0)
      theorem WithTop.map_eq_one_iff {β : Type v} {α : Type u_1} {f : αβ} {v : WithTop α} [One β] :
      map f v = 1 (x : α), v = x f x = 1
      theorem WithTop.map_eq_zero_iff {β : Type v} {α : Type u_1} {f : αβ} {v : WithTop α} [Zero β] :
      map f v = 0 (x : α), v = x f x = 0
      theorem WithTop.one_eq_map_iff {β : Type v} {α : Type u_1} {f : αβ} {v : WithTop α} [One β] :
      1 = map f v (x : α), v = x f x = 1
      theorem WithTop.zero_eq_map_iff {β : Type v} {α : Type u_1} {f : αβ} {v : WithTop α} [Zero β] :
      0 = map f v (x : α), v = x f x = 0
      instance WithTop.zeroLEOneClass {α : Type u} [One α] [Zero α] [LE α] [ZeroLEOneClass α] :
      instance WithTop.add {α : Type u} [Add α] :
      Equations
        @[simp]
        theorem WithTop.coe_add {α : Type u} [Add α] (a b : α) :
        ↑(a + b) = a + b
        @[simp]
        theorem WithTop.top_add {α : Type u} [Add α] (x : WithTop α) :
        @[simp]
        theorem WithTop.add_top {α : Type u} [Add α] (x : WithTop α) :
        @[simp]
        theorem WithTop.add_eq_top {α : Type u} [Add α] {x y : WithTop α} :
        x + y = x = y =
        theorem WithTop.add_ne_top {α : Type u} [Add α] {x y : WithTop α} :
        @[simp]
        theorem WithTop.add_lt_top {α : Type u} [Add α] {x y : WithTop α} [LT α] :
        x + y < x < y <
        theorem WithTop.add_eq_coe {α : Type u} [Add α] {a b : WithTop α} {c : α} :
        a + b = c (a' : α), (b' : α), a' = a b' = b a' + b' = c
        theorem WithTop.add_coe_eq_top_iff {α : Type u} [Add α] {x : WithTop α} {b : α} :
        x + b = x =
        theorem WithTop.coe_add_eq_top_iff {α : Type u} [Add α] {y : WithTop α} {a : α} :
        a + y = y =
        theorem WithTop.add_right_inj {α : Type u} [Add α] {x y z : WithTop α} [IsRightCancelAdd α] (hz : z ) :
        x + z = y + z x = y
        theorem WithTop.add_right_cancel {α : Type u} [Add α] {x y z : WithTop α} [IsRightCancelAdd α] (hz : z ) (h : x + z = y + z) :
        x = y
        theorem WithTop.add_left_inj {α : Type u} [Add α] {x y z : WithTop α} [IsLeftCancelAdd α] (hx : x ) :
        x + y = x + z y = z
        theorem WithTop.add_left_cancel {α : Type u} [Add α] {x y z : WithTop α} [IsLeftCancelAdd α] (hx : x ) (h : x + y = x + z) :
        y = z
        @[deprecated WithTop.add_left_inj (since := "2025-02-19")]
        theorem WithTop.add_left_cancel_iff {α : Type u} [Add α] {x y z : WithTop α} [IsLeftCancelAdd α] (hx : x ) :
        x + y = x + z y = z

        Alias of WithTop.add_left_inj.

        @[deprecated WithTop.add_right_inj (since := "2025-02-19")]
        theorem WithTop.add_right_cancel_iff {α : Type u} [Add α] {x y z : WithTop α} [IsRightCancelAdd α] (hz : z ) :
        x + z = y + z x = y

        Alias of WithTop.add_right_inj.

        instance WithTop.addLeftMono {α : Type u} [Add α] [LE α] [AddLeftMono α] :
        instance WithTop.addRightMono {α : Type u} [Add α] [LE α] [AddRightMono α] :
        theorem WithTop.le_of_add_le_add_left {α : Type u} [Add α] {x y z : WithTop α} [LE α] [AddLeftReflectLE α] (hx : x ) :
        x + y x + zy z
        theorem WithTop.le_of_add_le_add_right {α : Type u} [Add α] {x y z : WithTop α} [LE α] [AddRightReflectLE α] (hz : z ) :
        x + z y + zx y
        theorem WithTop.add_lt_add_left {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddLeftStrictMono α] (hx : x ) :
        y < zx + y < x + z
        theorem WithTop.add_lt_add_right {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddRightStrictMono α] (hz : z ) :
        x < yx + z < y + z
        theorem WithTop.add_le_add_iff_left {α : Type u} [Add α] {x y z : WithTop α} [LE α] [AddLeftMono α] [AddLeftReflectLE α] (hx : x ) :
        x + y x + z y z
        theorem WithTop.add_le_add_iff_right {α : Type u} [Add α] {x y z : WithTop α} [LE α] [AddRightMono α] [AddRightReflectLE α] (hz : z ) :
        x + z y + z x y
        theorem WithTop.add_lt_add_iff_left {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (hx : x ) :
        x + y < x + z y < z
        theorem WithTop.add_lt_add_iff_right {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddRightStrictMono α] [AddRightReflectLT α] (hz : z ) :
        x + z < y + z x < y
        theorem WithTop.add_lt_add_of_le_of_lt {α : Type u} [Add α] {w x y z : WithTop α} [Preorder α] [AddLeftStrictMono α] [AddRightMono α] (hw : w ) (hwy : w y) (hxz : x < z) :
        w + x < y + z
        theorem WithTop.add_lt_add_of_lt_of_le {α : Type u} [Add α] {w x y z : WithTop α} [Preorder α] [AddLeftMono α] [AddRightStrictMono α] (hx : x ) (hwy : w < y) (hxz : x z) :
        w + x < y + z
        theorem WithTop.addLECancellable_of_ne_top {α : Type u} [Add α] {x : WithTop α} [LE α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (hx : x ) :
        theorem WithTop.addLECancellable_of_lt_top {α : Type u} [Add α] {x : WithTop α} [Preorder α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (hx : x < ) :
        theorem WithTop.addLECancellable_coe {α : Type u} [Add α] [LE α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
        theorem WithTop.addLECancellable_iff_ne_top {α : Type u} [Add α] {x : WithTop α} [Nonempty α] [Preorder α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
        @[simp]
        theorem WithTop.map_add {α : Type u} {β : Type v} [Add α] {F : Type u_1} [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a b : WithTop α) :
        map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b
        Equations
          Equations
            instance WithTop.addMonoid {α : Type u} [AddMonoid α] :
            Equations
              @[simp]
              theorem WithTop.coe_nsmul {α : Type u} [AddMonoid α] (a : α) (n : ) :
              ↑(n a) = n a
              def WithTop.addHom {α : Type u} [AddMonoid α] :

              Coercion from α to WithTop α as an AddMonoidHom.

              Equations
                Instances For
                  @[simp]
                  theorem WithTop.coe_addHom {α : Type u} [AddMonoid α] :
                  @[simp]
                  theorem WithTop.coe_natCast {α : Type u} [AddMonoidWithOne α] (n : ) :
                  n = n
                  @[simp]
                  theorem WithTop.top_ne_natCast {α : Type u} [AddMonoidWithOne α] (n : ) :
                  n
                  @[simp]
                  theorem WithTop.natCast_ne_top {α : Type u} [AddMonoidWithOne α] (n : ) :
                  n
                  @[simp]
                  theorem WithTop.natCast_lt_top {α : Type u} [AddMonoidWithOne α] [LT α] (n : ) :
                  n <
                  @[simp]
                  theorem WithTop.coe_ofNat {α : Type u} [AddMonoidWithOne α] (n : ) [n.AtLeastTwo] :
                  @[simp]
                  theorem WithTop.coe_eq_ofNat {α : Type u} [AddMonoidWithOne α] (n : ) [n.AtLeastTwo] (m : α) :
                  @[simp]
                  theorem WithTop.ofNat_eq_coe {α : Type u} [AddMonoidWithOne α] (n : ) [n.AtLeastTwo] (m : α) :
                  @[simp]
                  theorem WithTop.map_ofNat {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : αβ} (n : ) [n.AtLeastTwo] :
                  map f (OfNat.ofNat n) = (f (OfNat.ofNat n))
                  @[simp]
                  theorem WithTop.map_natCast {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : αβ} (n : ) :
                  map f n = (f n)
                  theorem WithTop.map_eq_ofNat_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : βα} {n : } [n.AtLeastTwo] {a : WithTop β} :
                  map f a = OfNat.ofNat n (x : β), a = x f x = n
                  theorem WithTop.ofNat_eq_map_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : βα} {n : } [n.AtLeastTwo] {a : WithTop β} :
                  OfNat.ofNat n = map f a (x : β), a = x f x = n
                  theorem WithTop.map_eq_natCast_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : βα} {n : } {a : WithTop β} :
                  map f a = n (x : β), a = x f x = n
                  theorem WithTop.natCast_eq_map_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : βα} {n : } {a : WithTop β} :
                  n = map f a (x : β), a = x f x = n
                  @[simp]
                  theorem WithTop.one_lt_top {α : Type u} [One α] [LT α] :
                  1 <
                  @[simp]
                  theorem WithTop.top_pos {α : Type u} [Zero α] [LT α] :
                  0 <
                  @[deprecated WithTop.top_pos (since := "2024-10-22")]
                  theorem WithTop.zero_lt_top {α : Type u} [Zero α] [LT α] :
                  0 <

                  Alias of WithTop.top_pos.

                  @[deprecated WithTop.coe_pos (since := "2024-10-22")]
                  theorem WithTop.zero_lt_coe {α : Type u} [Zero α] [LT α] (a : α) :
                  0 < a 0 < a
                  def OneHom.withTopMap {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) :

                  A version of WithTop.map for OneHoms.

                  Equations
                    Instances For
                      def ZeroHom.withTopMap {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) :

                      A version of WithTop.map for ZeroHoms

                      Equations
                        Instances For
                          @[simp]
                          theorem OneHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) :
                          @[simp]
                          theorem ZeroHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) :
                          def AddHom.withTopMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :

                          A version of WithTop.map for AddHoms.

                          Equations
                            Instances For
                              @[simp]
                              theorem AddHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :
                              def AddMonoidHom.withTopMap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :

                              A version of WithTop.map for AddMonoidHoms.

                              Equations
                                Instances For
                                  @[simp]
                                  theorem AddMonoidHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                  instance WithBot.one {α : Type u} [One α] :
                                  Equations
                                    instance WithBot.zero {α : Type u} [Zero α] :
                                    Equations
                                      @[simp]
                                      theorem WithBot.coe_one {α : Type u} [One α] :
                                      1 = 1
                                      @[simp]
                                      theorem WithBot.coe_zero {α : Type u} [Zero α] :
                                      0 = 0
                                      @[simp]
                                      theorem WithBot.coe_eq_one {α : Type u} [One α] {a : α} :
                                      a = 1 a = 1
                                      @[simp]
                                      theorem WithBot.coe_eq_zero {α : Type u} [Zero α] {a : α} :
                                      a = 0 a = 0
                                      @[simp]
                                      theorem WithBot.one_eq_coe {α : Type u} [One α] {a : α} :
                                      1 = a a = 1
                                      @[simp]
                                      theorem WithBot.zero_eq_coe {α : Type u} [Zero α] {a : α} :
                                      0 = a a = 0
                                      @[simp]
                                      theorem WithBot.bot_ne_one {α : Type u} [One α] :
                                      @[simp]
                                      theorem WithBot.bot_ne_zero {α : Type u} [Zero α] :
                                      @[simp]
                                      theorem WithBot.one_ne_bot {α : Type u} [One α] :
                                      @[simp]
                                      theorem WithBot.zero_ne_bot {α : Type u} [Zero α] :
                                      @[simp]
                                      theorem WithBot.unbot_one {α : Type u} [One α] :
                                      unbot 1 = 1
                                      @[simp]
                                      theorem WithBot.unbot_zero {α : Type u} [Zero α] :
                                      unbot 0 = 0
                                      @[simp]
                                      theorem WithBot.unbotD_one {α : Type u} [One α] (d : α) :
                                      unbotD d 1 = 1
                                      @[simp]
                                      theorem WithBot.unbotD_zero {α : Type u} [Zero α] (d : α) :
                                      unbotD d 0 = 0
                                      @[deprecated WithBot.unbotD_zero (since := "2025-02-06")]
                                      theorem WithBot.unbot_zero' {α : Type u} [Zero α] (d : α) :
                                      unbotD d 0 = 0

                                      Alias of WithBot.unbotD_zero.

                                      @[deprecated WithBot.unbotD_one (since := "2025-02-06")]
                                      theorem WithBot.unbot_one' {α : Type u} [One α] (d : α) :
                                      unbotD d 1 = 1

                                      Alias of WithBot.unbotD_one.

                                      @[simp]
                                      theorem WithBot.one_le_coe {α : Type u} [One α] {a : α} [LE α] :
                                      1 a 1 a
                                      @[simp]
                                      theorem WithBot.coe_nonneg {α : Type u} [Zero α] {a : α} [LE α] :
                                      0 a 0 a
                                      @[simp]
                                      theorem WithBot.coe_le_one {α : Type u} [One α] {a : α} [LE α] :
                                      a 1 a 1
                                      @[simp]
                                      theorem WithBot.coe_le_zero {α : Type u} [Zero α] {a : α} [LE α] :
                                      a 0 a 0
                                      @[simp]
                                      theorem WithBot.one_lt_coe {α : Type u} [One α] {a : α} [LT α] :
                                      1 < a 1 < a
                                      @[simp]
                                      theorem WithBot.coe_pos {α : Type u} [Zero α] {a : α} [LT α] :
                                      0 < a 0 < a
                                      @[simp]
                                      theorem WithBot.coe_lt_one {α : Type u} [One α] {a : α} [LT α] :
                                      a < 1 a < 1
                                      @[simp]
                                      theorem WithBot.coe_lt_zero {α : Type u} [Zero α] {a : α} [LT α] :
                                      a < 0 a < 0
                                      @[simp]
                                      theorem WithBot.map_one {α : Type u} [One α] {β : Type u_1} (f : αβ) :
                                      map f 1 = (f 1)
                                      @[simp]
                                      theorem WithBot.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : αβ) :
                                      map f 0 = (f 0)
                                      theorem WithBot.map_eq_one_iff {β : Type v} {α : Type u_1} {f : αβ} {v : WithBot α} [One β] :
                                      map f v = 1 (x : α), v = x f x = 1
                                      theorem WithBot.map_eq_zero_iff {β : Type v} {α : Type u_1} {f : αβ} {v : WithBot α} [Zero β] :
                                      map f v = 0 (x : α), v = x f x = 0
                                      theorem WithBot.one_eq_map_iff {β : Type v} {α : Type u_1} {f : αβ} {v : WithBot α} [One β] :
                                      1 = map f v (x : α), v = x f x = 1
                                      theorem WithBot.zero_eq_map_iff {β : Type v} {α : Type u_1} {f : αβ} {v : WithBot α} [Zero β] :
                                      0 = map f v (x : α), v = x f x = 0
                                      instance WithBot.zeroLEOneClass {α : Type u} [One α] [Zero α] [LE α] [ZeroLEOneClass α] :
                                      instance WithBot.add {α : Type u} [Add α] :
                                      Equations
                                        @[simp]
                                        theorem WithBot.coe_add {α : Type u} [Add α] (a b : α) :
                                        ↑(a + b) = a + b
                                        @[simp]
                                        theorem WithBot.bot_add {α : Type u} [Add α] (x : WithBot α) :
                                        @[simp]
                                        theorem WithBot.add_bot {α : Type u} [Add α] (x : WithBot α) :
                                        @[simp]
                                        theorem WithBot.add_eq_bot {α : Type u} [Add α] {x y : WithBot α} :
                                        x + y = x = y =
                                        theorem WithBot.add_ne_bot {α : Type u} [Add α] {x y : WithBot α} :
                                        @[simp]
                                        theorem WithBot.bot_lt_add {α : Type u} [Add α] {x y : WithBot α} [LT α] :
                                        < x + y < x < y
                                        theorem WithBot.add_eq_coe {α : Type u} [Add α] {a b : WithBot α} {c : α} :
                                        a + b = c (a' : α), (b' : α), a' = a b' = b a' + b' = c
                                        theorem WithBot.add_coe_eq_bot_iff {α : Type u} [Add α] {x : WithBot α} {b : α} :
                                        x + b = x =
                                        theorem WithBot.coe_add_eq_bot_iff {α : Type u} [Add α] {y : WithBot α} {a : α} :
                                        a + y = y =
                                        theorem WithBot.add_right_inj {α : Type u} [Add α] {x y z : WithBot α} [IsRightCancelAdd α] (hz : z ) :
                                        x + z = y + z x = y
                                        theorem WithBot.add_right_cancel {α : Type u} [Add α] {x y z : WithBot α} [IsRightCancelAdd α] (hz : z ) (h : x + z = y + z) :
                                        x = y
                                        theorem WithBot.add_left_inj {α : Type u} [Add α] {x y z : WithBot α} [IsLeftCancelAdd α] (hx : x ) :
                                        x + y = x + z y = z
                                        theorem WithBot.add_left_cancel {α : Type u} [Add α] {x y z : WithBot α} [IsLeftCancelAdd α] (hx : x ) (h : x + y = x + z) :
                                        y = z
                                        @[deprecated WithBot.add_left_inj (since := "2025-02-19")]
                                        theorem WithBot.add_left_cancel_iff {α : Type u} [Add α] {x y z : WithBot α} [IsLeftCancelAdd α] (hx : x ) :
                                        x + y = x + z y = z

                                        Alias of WithBot.add_left_inj.

                                        @[deprecated WithBot.add_right_inj (since := "2025-02-19")]
                                        theorem WithBot.add_right_cancel_iff {α : Type u} [Add α] {x y z : WithBot α} [IsRightCancelAdd α] (hz : z ) :
                                        x + z = y + z x = y

                                        Alias of WithBot.add_right_inj.

                                        instance WithBot.addLeftMono {α : Type u} [Add α] [LE α] [AddLeftMono α] :
                                        instance WithBot.addRightMono {α : Type u} [Add α] [LE α] [AddRightMono α] :
                                        theorem WithBot.le_of_add_le_add_left {α : Type u} [Add α] {x y z : WithBot α} [LE α] [AddLeftReflectLE α] (hx : x ) :
                                        x + y x + zy z
                                        theorem WithBot.le_of_add_le_add_right {α : Type u} [Add α] {x y z : WithBot α} [LE α] [AddRightReflectLE α] (hz : z ) :
                                        x + z y + zx y
                                        theorem WithBot.add_lt_add_left {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddLeftStrictMono α] (hx : x ) :
                                        y < zx + y < x + z
                                        theorem WithBot.add_lt_add_right {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddRightStrictMono α] (hz : z ) :
                                        x < yx + z < y + z
                                        theorem WithBot.add_le_add_iff_left {α : Type u} [Add α] {x y z : WithBot α} [LE α] [AddLeftMono α] [AddLeftReflectLE α] (hx : x ) :
                                        x + y x + z y z
                                        theorem WithBot.add_le_add_iff_right {α : Type u} [Add α] {x y z : WithBot α} [LE α] [AddRightMono α] [AddRightReflectLE α] (hz : z ) :
                                        x + z y + z x y
                                        theorem WithBot.add_lt_add_iff_left {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (hx : x ) :
                                        x + y < x + z y < z
                                        theorem WithBot.add_lt_add_iff_right {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddRightStrictMono α] [AddRightReflectLT α] (hz : z ) :
                                        x + z < y + z x < y
                                        theorem WithBot.add_lt_add_of_le_of_lt {α : Type u} [Add α] {w x y z : WithBot α} [Preorder α] [AddLeftStrictMono α] [AddRightMono α] (hw : w ) (hwy : w y) (hxz : x < z) :
                                        w + x < y + z
                                        theorem WithBot.add_lt_add_of_lt_of_le {α : Type u} [Add α] {w x y z : WithBot α} [Preorder α] [AddLeftMono α] [AddRightStrictMono α] (hx : x ) (hwy : w < y) (hxz : x z) :
                                        w + x < y + z
                                        theorem WithBot.addLECancellable_of_ne_bot {α : Type u} [Add α] {x : WithBot α} [LE α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (hx : x ) :
                                        theorem WithBot.addLECancellable_of_lt_bot {α : Type u} [Add α] {x : WithBot α} [Preorder α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (hx : x < ) :
                                        theorem WithBot.addLECancellable_coe {α : Type u} [Add α] [LE α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
                                        theorem WithBot.addLECancellable_iff_ne_bot {α : Type u} [Add α] {x : WithBot α} [Nonempty α] [Preorder α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
                                        @[simp]
                                        theorem WithBot.map_add {α : Type u} {β : Type v} [Add α] {F : Type u_1} [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a b : WithBot α) :
                                        map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b
                                        Equations
                                          instance WithBot.addMonoid {α : Type u} [AddMonoid α] :
                                          Equations
                                            def WithBot.addHom {α : Type u} [AddMonoid α] :

                                            Coercion from α to WithBot α as an AddMonoidHom.

                                            Equations
                                              Instances For
                                                @[simp]
                                                theorem WithBot.coe_addHom {α : Type u} [AddMonoid α] :
                                                @[simp]
                                                theorem WithBot.coe_nsmul {α : Type u} [AddMonoid α] (a : α) (n : ) :
                                                ↑(n a) = n a
                                                theorem WithBot.coe_natCast {α : Type u} [AddMonoidWithOne α] (n : ) :
                                                n = n
                                                @[simp]
                                                theorem WithBot.natCast_ne_bot {α : Type u} [AddMonoidWithOne α] (n : ) :
                                                n
                                                @[simp]
                                                theorem WithBot.bot_ne_natCast {α : Type u} [AddMonoidWithOne α] (n : ) :
                                                n
                                                @[simp]
                                                theorem WithBot.coe_ofNat {α : Type u} [AddMonoidWithOne α] (n : ) [n.AtLeastTwo] :
                                                @[simp]
                                                theorem WithBot.coe_eq_ofNat {α : Type u} [AddMonoidWithOne α] (n : ) [n.AtLeastTwo] (m : α) :
                                                @[simp]
                                                theorem WithBot.ofNat_eq_coe {α : Type u} [AddMonoidWithOne α] (n : ) [n.AtLeastTwo] (m : α) :
                                                @[simp]
                                                theorem WithBot.map_ofNat {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : αβ} (n : ) [n.AtLeastTwo] :
                                                map f (OfNat.ofNat n) = (f (OfNat.ofNat n))
                                                @[simp]
                                                theorem WithBot.map_natCast {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : αβ} (n : ) :
                                                map f n = (f n)
                                                theorem WithBot.map_eq_ofNat_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : βα} {n : } [n.AtLeastTwo] {a : WithBot β} :
                                                map f a = OfNat.ofNat n (x : β), a = x f x = n
                                                theorem WithBot.ofNat_eq_map_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : βα} {n : } [n.AtLeastTwo] {a : WithBot β} :
                                                OfNat.ofNat n = map f a (x : β), a = x f x = n
                                                theorem WithBot.map_eq_natCast_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : βα} {n : } {a : WithBot β} :
                                                map f a = n (x : β), a = x f x = n
                                                theorem WithBot.natCast_eq_map_iff {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : βα} {n : } {a : WithBot β} :
                                                n = map f a (x : β), a = x f x = n
                                                def OneHom.withBotMap {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) :

                                                A version of WithBot.map for OneHoms.

                                                Equations
                                                  Instances For
                                                    def ZeroHom.withBotMap {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) :

                                                    A version of WithBot.map for ZeroHoms

                                                    Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem ZeroHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) :
                                                        @[simp]
                                                        theorem OneHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) :
                                                        def AddHom.withBotMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :

                                                        A version of WithBot.map for AddHoms.

                                                        Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem AddHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :
                                                            def AddMonoidHom.withBotMap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :

                                                            A version of WithBot.map for AddMonoidHoms.

                                                            Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem AddMonoidHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :