Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Adjoining top/bottom elements to ordered monoids. #

instance WithTop.zero {α : Type u} [Zero α] :
Equations
  • WithTop.zero = { zero := 0 }
instance WithTop.one {α : Type u} [One α] :
Equations
  • WithTop.one = { one := 1 }
@[simp]
theorem WithTop.coe_zero {α : Type u} [Zero α] :
0 = 0
@[simp]
theorem WithTop.coe_one {α : Type u} [One α] :
1 = 1
@[simp]
theorem WithTop.coe_eq_zero {α : Type u} [Zero α] {a : α} :
a = 0 a = 0
@[simp]
theorem WithTop.coe_eq_one {α : Type u} [One α] {a : α} :
a = 1 a = 1
@[simp]
theorem WithTop.zero_eq_coe {α : Type u} [Zero α] {a : α} :
0 = a a = 0
@[simp]
theorem WithTop.one_eq_coe {α : Type u} [One α] {a : α} :
1 = a a = 1
@[simp]
theorem WithTop.top_ne_zero {α : Type u} [Zero α] :
@[simp]
theorem WithTop.top_ne_one {α : Type u} [One α] :
@[simp]
theorem WithTop.zero_ne_top {α : Type u} [Zero α] :
@[simp]
theorem WithTop.one_ne_top {α : Type u} [One α] :
@[simp]
theorem WithTop.untop_zero {α : Type u} [Zero α] :
@[simp]
theorem WithTop.untop_one {α : Type u} [One α] :
@[simp]
theorem WithTop.untop_zero' {α : Type u} [Zero α] (d : α) :
@[simp]
theorem WithTop.untop_one' {α : Type u} [One α] (d : α) :
@[simp]
theorem WithTop.coe_nonneg {α : Type u} [Zero α] [LE α] {a : α} :
0 a 0 a
@[simp]
theorem WithTop.one_le_coe {α : Type u} [One α] [LE α] {a : α} :
1 a 1 a
@[simp]
theorem WithTop.coe_le_zero {α : Type u} [Zero α] [LE α] {a : α} :
a 0 a 0
@[simp]
theorem WithTop.coe_le_one {α : Type u} [One α] [LE α] {a : α} :
a 1 a 1
@[simp]
theorem WithTop.coe_pos {α : Type u} [Zero α] [LT α] {a : α} :
0 < a 0 < a
@[simp]
theorem WithTop.one_lt_coe {α : Type u} [One α] [LT α] {a : α} :
1 < a 1 < a
@[simp]
theorem WithTop.coe_lt_zero {α : Type u} [Zero α] [LT α] {a : α} :
a < 0 a < 0
@[simp]
theorem WithTop.coe_lt_one {α : Type u} [One α] [LT α] {a : α} :
a < 1 a < 1
@[simp]
theorem WithTop.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : αβ) :
WithTop.map f 0 = (f 0)
@[simp]
theorem WithTop.map_one {α : Type u} [One α] {β : Type u_1} (f : αβ) :
WithTop.map f 1 = (f 1)
instance WithTop.zeroLEOneClass {α : Type u} [One α] [Zero α] [LE α] [ZeroLEOneClass α] :
Equations
  • =
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 α] (a : WithTop α) :
@[simp]
theorem WithTop.add_top {α : Type u} [Add α] (a : WithTop α) :
@[simp]
theorem WithTop.add_eq_top {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} :
a + b = a = b =
theorem WithTop.add_ne_top {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} :
theorem WithTop.add_lt_top {α : Type u} [Add α] [LT α] {a : WithTop α} {b : WithTop α} :
a + b < a < b <
theorem WithTop.add_eq_coe {α : Type u} [Add α] {a : WithTop α} {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 α} {y : α} :
x + y = x =
theorem WithTop.coe_add_eq_top_iff {α : Type u} [Add α] {x : α} {y : WithTop α} :
x + y = y =
theorem WithTop.add_right_cancel_iff {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsRightCancelAdd α] (ha : a ) :
b + a = c + a b = c
theorem WithTop.add_right_cancel {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsRightCancelAdd α] (ha : a ) (h : b + a = c + a) :
b = c
theorem WithTop.add_left_cancel_iff {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsLeftCancelAdd α] (ha : a ) :
a + b = a + c b = c
theorem WithTop.add_left_cancel {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsLeftCancelAdd α] (ha : a ) (h : a + b = a + c) :
b = c
instance WithTop.covariantClass_add_le {α : Type u} [Add α] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :
CovariantClass (WithTop α) (WithTop α) (fun (x x_1 : WithTop α) => x + x_1) fun (x x_1 : WithTop α) => x x_1
Equations
  • =
instance WithTop.covariantClass_swap_add_le {α : Type u} [Add α] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :
CovariantClass (WithTop α) (WithTop α) (Function.swap fun (x x_1 : WithTop α) => x + x_1) fun (x x_1 : WithTop α) => x x_1
Equations
  • =
instance WithTop.contravariantClass_add_lt {α : Type u} [Add α] [LT α] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] :
ContravariantClass (WithTop α) (WithTop α) (fun (x x_1 : WithTop α) => x + x_1) fun (x x_1 : WithTop α) => x < x_1
Equations
  • =
instance WithTop.contravariantClass_swap_add_lt {α : Type u} [Add α] [LT α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] :
ContravariantClass (WithTop α) (WithTop α) (Function.swap fun (x x_1 : WithTop α) => x + x_1) fun (x x_1 : WithTop α) => x < x_1
Equations
  • =
theorem WithTop.le_of_add_le_add_left {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LE α] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (ha : a ) (h : a + b a + c) :
b c
theorem WithTop.le_of_add_le_add_right {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (ha : a ) (h : b + a c + a) :
b c
theorem WithTop.add_lt_add_left {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LT α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (ha : a ) (h : b < c) :
a + b < a + c
theorem WithTop.add_lt_add_right {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LT α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (ha : a ) (h : b < c) :
b + a < c + a
theorem WithTop.add_le_add_iff_left {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (ha : a ) :
a + b a + c b c
theorem WithTop.add_le_add_iff_right {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (ha : a ) :
b + a c + a b c
theorem WithTop.add_lt_add_iff_left {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LT α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (ha : a ) :
a + b < a + c b < c
theorem WithTop.add_lt_add_iff_right {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LT α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (ha : a ) :
b + a < c + a b < c
theorem WithTop.add_lt_add_of_le_of_lt {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} {d : WithTop α} [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (ha : a ) (hab : a b) (hcd : c < d) :
a + c < b + d
theorem WithTop.add_lt_add_of_lt_of_le {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} {d : WithTop α} [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (hc : c ) (hab : a < b) (hcd : c d) :
a + c < b + d
@[simp]
theorem WithTop.map_add {α : Type u} {β : Type v} [Add α] {F : Type u_1} [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a : WithTop α) (b : WithTop α) :
WithTop.map (⇑f) (a + b) = WithTop.map (⇑f) a + WithTop.map (⇑f) b
Equations
Equations
Equations
  • WithTop.addZeroClass = let __src := WithTop.zero; let __src_1 := WithTop.add; AddZeroClass.mk
instance WithTop.addMonoid {α : Type u} [AddMonoid α] :
Equations
  • One or more equations did not get rendered due to their size.
@[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
  • WithTop.addHom = { toFun := WithTop.some, map_zero' := , map_add' := }
Instances For
    @[simp]
    theorem WithTop.coe_addHom {α : Type u} [AddMonoid α] :
    WithTop.addHom = WithTop.some
    Equations
    • WithTop.addCommMonoid = let __src := WithTop.addMonoid; let __src_1 := WithTop.addCommSemigroup; AddCommMonoid.mk
    Equations
    • WithTop.addMonoidWithOne = let __src := WithTop.one; let __src_1 := WithTop.addMonoid; AddMonoidWithOne.mk
    @[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 <
    @[deprecated WithTop.coe_natCast]
    theorem WithTop.coe_nat {α : Type u} [AddMonoidWithOne α] (n : ) :
    n = n

    Alias of WithTop.coe_natCast.

    @[deprecated WithTop.natCast_ne_top]
    theorem WithTop.nat_ne_top {α : Type u} [AddMonoidWithOne α] (n : ) :
    n

    Alias of WithTop.natCast_ne_top.

    @[deprecated WithTop.top_ne_natCast]
    theorem WithTop.top_ne_nat {α : Type u} [AddMonoidWithOne α] (n : ) :
    n

    Alias of WithTop.top_ne_natCast.

    @[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.ofNat_ne_top {α : Type u} [AddMonoidWithOne α] (n : ) [n.AtLeastTwo] :
    @[simp]
    theorem WithTop.top_ne_ofNat {α : Type u} [AddMonoidWithOne α] (n : ) [n.AtLeastTwo] :
    Equations
    • =
    Equations
    • WithTop.addCommMonoidWithOne = let __src := WithTop.addMonoidWithOne; let __src_1 := WithTop.addCommMonoid; AddCommMonoidWithOne.mk
    instance WithTop.existsAddOfLE {α : Type u} [LE α] [Add α] [ExistsAddOfLE α] :
    Equations
    • =
    @[simp]
    theorem WithTop.zero_lt_top {α : Type u} [Zero α] [LT α] :
    0 <
    theorem WithTop.zero_lt_coe {α : Type u} [Zero α] [LT α] (a : α) :
    0 < a 0 < a
    theorem ZeroHom.withTopMap.proof_1 {M : Type u_2} {N : Type u_1} [Zero M] [Zero N] (f : ZeroHom M N) :
    WithTop.map (⇑f) 0 = 0
    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
    • f.withTopMap = { toFun := WithTop.map f, map_zero' := }
    Instances For
      @[simp]
      theorem ZeroHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) :
      f.withTopMap = WithTop.map f
      @[simp]
      theorem OneHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) :
      f.withTopMap = WithTop.map f
      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
      • f.withTopMap = { toFun := WithTop.map f, map_one' := }
      Instances For
        @[simp]
        theorem AddHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
        f.withTopMap = WithTop.map f
        def AddHom.withTopMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :

        A version of WithTop.map for AddHoms.

        Equations
        • f.withTopMap = { toFun := WithTop.map f, map_add' := }
        Instances For
          @[simp]
          theorem AddMonoidHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
          f.withTopMap = WithTop.map f
          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
          • f.withTopMap = let __src := (↑f).withTopMap; let __src := (↑f).withTopMap; { toFun := WithTop.map f, map_zero' := , map_add' := }
          Instances For
            instance WithBot.zero {α : Type u} [Zero α] :
            Equations
            • WithBot.zero = WithTop.zero
            instance WithBot.one {α : Type u} [One α] :
            Equations
            • WithBot.one = WithTop.one
            @[simp]
            theorem WithBot.coe_zero {α : Type u} [Zero α] :
            0 = 0
            @[simp]
            theorem WithBot.coe_one {α : Type u} [One α] :
            1 = 1
            @[simp]
            theorem WithBot.coe_eq_zero {α : Type u} [Zero α] {a : α} :
            a = 0 a = 0
            @[simp]
            theorem WithBot.coe_eq_one {α : Type u} [One α] {a : α} :
            a = 1 a = 1
            @[simp]
            theorem WithBot.zero_eq_coe {α : Type u} [Zero α] {a : α} :
            0 = a a = 0
            @[simp]
            theorem WithBot.one_eq_coe {α : Type u} [One α] {a : α} :
            1 = a a = 1
            @[simp]
            theorem WithBot.bot_ne_zero {α : Type u} [Zero α] :
            @[simp]
            theorem WithBot.bot_ne_one {α : Type u} [One α] :
            @[simp]
            theorem WithBot.zero_ne_bot {α : Type u} [Zero α] :
            @[simp]
            theorem WithBot.one_ne_bot {α : Type u} [One α] :
            @[simp]
            theorem WithBot.unbot_zero {α : Type u} [Zero α] :
            @[simp]
            theorem WithBot.unbot_one {α : Type u} [One α] :
            @[simp]
            theorem WithBot.unbot_zero' {α : Type u} [Zero α] (d : α) :
            @[simp]
            theorem WithBot.unbot_one' {α : Type u} [One α] (d : α) :
            @[simp]
            theorem WithBot.coe_nonneg {α : Type u} [Zero α] {a : α} [LE α] :
            0 a 0 a
            @[simp]
            theorem WithBot.one_le_coe {α : Type u} [One α] {a : α} [LE α] :
            1 a 1 a
            @[simp]
            theorem WithBot.coe_le_zero {α : Type u} [Zero α] {a : α} [LE α] :
            a 0 a 0
            @[simp]
            theorem WithBot.coe_le_one {α : Type u} [One α] {a : α} [LE α] :
            a 1 a 1
            @[simp]
            theorem WithBot.coe_pos {α : Type u} [Zero α] {a : α} [LT α] :
            0 < a 0 < a
            @[simp]
            theorem WithBot.one_lt_coe {α : Type u} [One α] {a : α} [LT α] :
            1 < a 1 < a
            @[simp]
            theorem WithBot.coe_lt_zero {α : Type u} [Zero α] {a : α} [LT α] :
            a < 0 a < 0
            @[simp]
            theorem WithBot.coe_lt_one {α : Type u} [One α] {a : α} [LT α] :
            a < 1 a < 1
            @[simp]
            theorem WithBot.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : αβ) :
            WithBot.map f 0 = (f 0)
            @[simp]
            theorem WithBot.map_one {α : Type u} [One α] {β : Type u_1} (f : αβ) :
            WithBot.map f 1 = (f 1)
            instance WithBot.zeroLEOneClass {α : Type u} [One α] [Zero α] [LE α] [ZeroLEOneClass α] :
            Equations
            • =
            instance WithBot.add {α : Type u} [Add α] :
            Equations
            • WithBot.add = WithTop.add
            Equations
            • WithBot.AddSemigroup = WithTop.addSemigroup
            Equations
            • WithBot.addCommSemigroup = WithTop.addCommSemigroup
            Equations
            • WithBot.addZeroClass = WithTop.addZeroClass
            instance WithBot.addMonoid {α : Type u} [AddMonoid α] :
            Equations
            • WithBot.addMonoid = WithTop.addMonoid
            def WithBot.addHom {α : Type u} [AddMonoid α] :

            Coercion from α to WithBot α as an AddMonoidHom.

            Equations
            • WithBot.addHom = { toFun := WithTop.some, map_zero' := , map_add' := }
            Instances For
              @[simp]
              theorem WithBot.coe_addHom {α : Type u} [AddMonoid α] :
              WithBot.addHom = WithBot.some
              @[simp]
              theorem WithBot.coe_nsmul {α : Type u} [AddMonoid α] (a : α) (n : ) :
              (n a) = n a
              Equations
              • WithBot.addCommMonoid = WithTop.addCommMonoid
              Equations
              • WithBot.addMonoidWithOne = WithTop.addMonoidWithOne
              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
              @[deprecated WithBot.coe_natCast]
              theorem WithBot.coe_nat {α : Type u} [AddMonoidWithOne α] (n : ) :
              n = n

              Alias of WithBot.coe_natCast.

              @[deprecated WithBot.natCast_ne_bot]
              theorem WithBot.nat_ne_bot {α : Type u} [AddMonoidWithOne α] (n : ) :
              n

              Alias of WithBot.natCast_ne_bot.

              @[deprecated WithBot.bot_ne_natCast]
              theorem WithBot.bot_ne_nat {α : Type u} [AddMonoidWithOne α] (n : ) :
              n

              Alias of WithBot.bot_ne_natCast.

              @[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.ofNat_ne_bot {α : Type u} [AddMonoidWithOne α] (n : ) [n.AtLeastTwo] :
              @[simp]
              theorem WithBot.bot_ne_ofNat {α : Type u} [AddMonoidWithOne α] (n : ) [n.AtLeastTwo] :
              Equations
              • =
              Equations
              • WithBot.addCommMonoidWithOne = WithTop.addCommMonoidWithOne
              @[simp]
              theorem WithBot.coe_add {α : Type u} [Add α] (a : α) (b : α) :
              (a + b) = a + b
              @[simp]
              theorem WithBot.bot_add {α : Type u} [Add α] (a : WithBot α) :
              @[simp]
              theorem WithBot.add_bot {α : Type u} [Add α] (a : WithBot α) :
              @[simp]
              theorem WithBot.add_eq_bot {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} :
              a + b = a = b =
              theorem WithBot.add_ne_bot {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} :
              theorem WithBot.bot_lt_add {α : Type u} [Add α] [LT α] {a : WithBot α} {b : WithBot α} :
              < a + b < a < b
              theorem WithBot.add_eq_coe {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {x : α} :
              a + b = x ∃ (a' : α), ∃ (b' : α), a' = a b' = b a' + b' = x
              theorem WithBot.add_coe_eq_bot_iff {α : Type u} [Add α] {a : WithBot α} {y : α} :
              a + y = a =
              theorem WithBot.coe_add_eq_bot_iff {α : Type u} [Add α] {b : WithBot α} {x : α} :
              x + b = b =
              theorem WithBot.add_right_cancel_iff {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsRightCancelAdd α] (ha : a ) :
              b + a = c + a b = c
              theorem WithBot.add_right_cancel {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsRightCancelAdd α] (ha : a ) (h : b + a = c + a) :
              b = c
              theorem WithBot.add_left_cancel_iff {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsLeftCancelAdd α] (ha : a ) :
              a + b = a + c b = c
              theorem WithBot.add_left_cancel {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsLeftCancelAdd α] (ha : a ) (h : a + b = a + c) :
              b = c
              @[simp]
              theorem WithBot.map_add {α : Type u} {β : Type v} [Add α] {F : Type u_1} [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a : WithBot α) (b : WithBot α) :
              WithBot.map (⇑f) (a + b) = WithBot.map (⇑f) a + WithBot.map (⇑f) b
              theorem ZeroHom.withBotMap.proof_1 {M : Type u_2} {N : Type u_1} [Zero M] [Zero N] (f : ZeroHom M N) :
              WithBot.map (⇑f) 0 = 0
              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
              • f.withBotMap = { toFun := WithBot.map f, map_zero' := }
              Instances For
                @[simp]
                theorem OneHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) :
                f.withBotMap = WithBot.map f
                @[simp]
                theorem ZeroHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) :
                f.withBotMap = WithBot.map f
                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
                • f.withBotMap = { toFun := WithBot.map f, map_one' := }
                Instances For
                  @[simp]
                  theorem AddHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
                  f.withBotMap = WithBot.map f
                  def AddHom.withBotMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :

                  A version of WithBot.map for AddHoms.

                  Equations
                  • f.withBotMap = { toFun := WithBot.map f, map_add' := }
                  Instances For
                    @[simp]
                    theorem AddMonoidHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                    f.withBotMap = WithBot.map f
                    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
                    • f.withBotMap = let __src := (↑f).withBotMap; let __src := (↑f).withBotMap; { toFun := WithBot.map f, map_zero' := , map_add' := }
                    Instances For
                      instance WithBot.covariantClass_add_le {α : Type u} [Add α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :
                      CovariantClass (WithBot α) (WithBot α) (fun (x x_1 : WithBot α) => x + x_1) fun (x x_1 : WithBot α) => x x_1
                      Equations
                      • =
                      instance WithBot.covariantClass_swap_add_le {α : Type u} [Add α] [Preorder α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :
                      CovariantClass (WithBot α) (WithBot α) (Function.swap fun (x x_1 : WithBot α) => x + x_1) fun (x x_1 : WithBot α) => x x_1
                      Equations
                      • =
                      instance WithBot.contravariantClass_add_lt {α : Type u} [Add α] [Preorder α] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] :
                      ContravariantClass (WithBot α) (WithBot α) (fun (x x_1 : WithBot α) => x + x_1) fun (x x_1 : WithBot α) => x < x_1
                      Equations
                      • =
                      instance WithBot.contravariantClass_swap_add_lt {α : Type u} [Add α] [Preorder α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] :
                      ContravariantClass (WithBot α) (WithBot α) (Function.swap fun (x x_1 : WithBot α) => x + x_1) fun (x x_1 : WithBot α) => x < x_1
                      Equations
                      • =
                      theorem WithBot.le_of_add_le_add_left {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (ha : a ) (h : a + b a + c) :
                      b c
                      theorem WithBot.le_of_add_le_add_right {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (ha : a ) (h : b + a c + a) :
                      b c
                      theorem WithBot.add_lt_add_left {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (ha : a ) (h : b < c) :
                      a + b < a + c
                      theorem WithBot.add_lt_add_right {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (ha : a ) (h : b < c) :
                      b + a < c + a
                      theorem WithBot.add_le_add_iff_left {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (ha : a ) :
                      a + b a + c b c
                      theorem WithBot.add_le_add_iff_right {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (ha : a ) :
                      b + a c + a b c
                      theorem WithBot.add_lt_add_iff_left {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (ha : a ) :
                      a + b < a + c b < c
                      theorem WithBot.add_lt_add_iff_right {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (ha : a ) :
                      b + a < c + a b < c
                      theorem WithBot.add_lt_add_of_le_of_lt {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} {d : WithBot α} [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (hb : b ) (hab : a b) (hcd : c < d) :
                      a + c < b + d
                      theorem WithBot.add_lt_add_of_lt_of_le {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} {d : WithBot α} [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (hd : d ) (hab : a < b) (hcd : c d) :
                      a + c < b + d