Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Adjoining top/bottom elements to ordered monoids. #

source
instance WithTop.zero {α : Type u} [Zero α] :
Zero (WithTop α)
Equations
  • WithTop.zero = { zero := ↑0 }
source
instance WithTop.one {α : Type u} [One α] :
One (WithTop α)
Equations
  • WithTop.one = { one := ↑1 }
source
@[simp]
theorem WithTop.coe_zero {α : Type u} [Zero α] :
↑0 = 0
source
@[simp]
theorem WithTop.coe_one {α : Type u} [One α] :
↑1 = 1
source
@[simp]
theorem WithTop.coe_eq_zero {α : Type u} [Zero α] {a : α} :
↑a = 0 ↔ a = 0
source
@[simp]
theorem WithTop.coe_eq_one {α : Type u} [One α] {a : α} :
↑a = 1 ↔ a = 1
source
@[simp]
theorem WithTop.zero_eq_coe {α : Type u} [Zero α] {a : α} :
0 = ↑a ↔ a = 0
source
@[simp]
theorem WithTop.one_eq_coe {α : Type u} [One α] {a : α} :
1 = ↑a ↔ a = 1
source
@[simp]
theorem WithTop.top_ne_zero {α : Type u} [Zero α] :
⊤ ≠ 0
source
@[simp]
theorem WithTop.top_ne_one {α : Type u} [One α] :
⊤ ≠ 1
source
@[simp]
theorem WithTop.zero_ne_top {α : Type u} [Zero α] :
0 ≠ ⊤
source
@[simp]
theorem WithTop.one_ne_top {α : Type u} [One α] :
1 ≠ ⊤
source
@[simp]
theorem WithTop.untop_zero {α : Type u} [Zero α] :
WithTop.untop 0 ⋯ = 0
source
@[simp]
theorem WithTop.untop_one {α : Type u} [One α] :
WithTop.untop 1 ⋯ = 1
source
@[simp]
theorem WithTop.untop_zero' {α : Type u} [Zero α] (d : α) :
WithTop.untop' d 0 = 0
source
@[simp]
theorem WithTop.untop_one' {α : Type u} [One α] (d : α) :
WithTop.untop' d 1 = 1
source
@[simp]
theorem WithTop.coe_nonneg {α : Type u} [Zero α] [LE α] {a : α} :
0 ≤ ↑a ↔ 0 ≤ a
source
@[simp]
theorem WithTop.one_le_coe {α : Type u} [One α] [LE α] {a : α} :
1 ≤ ↑a ↔ 1 ≤ a
source
@[simp]
theorem WithTop.coe_le_zero {α : Type u} [Zero α] [LE α] {a : α} :
↑a ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem WithTop.coe_le_one {α : Type u} [One α] [LE α] {a : α} :
↑a ≤ 1 ↔ a ≤ 1
source
@[simp]
theorem WithTop.coe_pos {α : Type u} [Zero α] [LT α] {a : α} :
0 < ↑a ↔ 0 < a
source
@[simp]
theorem WithTop.one_lt_coe {α : Type u} [One α] [LT α] {a : α} :
1 < ↑a ↔ 1 < a
source
@[simp]
theorem WithTop.coe_lt_zero {α : Type u} [Zero α] [LT α] {a : α} :
↑a < 0 ↔ a < 0
source
@[simp]
theorem WithTop.coe_lt_one {α : Type u} [One α] [LT α] {a : α} :
↑a < 1 ↔ a < 1
source
@[simp]
theorem WithTop.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : α → β) :
WithTop.map f 0 = ↑(f 0)
source
@[simp]
theorem WithTop.map_one {α : Type u} [One α] {β : Type u_1} (f : α → β) :
WithTop.map f 1 = ↑(f 1)
source
instance WithTop.zeroLEOneClass {α : Type u} [One α] [Zero α] [LE α] [ZeroLEOneClass α] :
ZeroLEOneClass (WithTop α)
Equations
  • ⋯ = ⋯
source
instance WithTop.add {α : Type u} [Add α] :
Add (WithTop α)
Equations
source
@[simp]
theorem WithTop.coe_add {α : Type u} [Add α] (a : α) (b : α) :
↑(a + b) = ↑a + ↑b
source
@[simp]
theorem WithTop.top_add {α : Type u} [Add α] (a : WithTop α) :
⊤ + a = ⊤
source
@[simp]
theorem WithTop.add_top {α : Type u} [Add α] (a : WithTop α) :
a + ⊤ = ⊤
source
@[simp]
theorem WithTop.add_eq_top {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} :
a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
source
theorem WithTop.add_ne_top {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} :
a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤
source
theorem WithTop.add_lt_top {α : Type u} [Add α] [LT α] {a : WithTop α} {b : WithTop α} :
a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤
source
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
source
theorem WithTop.add_coe_eq_top_iff {α : Type u} [Add α] {x : WithTop α} {y : α} :
x + ↑y = ⊤ ↔ x = ⊤
source
theorem WithTop.coe_add_eq_top_iff {α : Type u} [Add α] {x : α} {y : WithTop α} :
↑x + y = ⊤ ↔ y = ⊤
source
theorem WithTop.add_right_cancel_iff {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsRightCancelAdd α] (ha : a ≠ ⊤) :
b + a = c + a ↔ b = c
source
theorem WithTop.add_right_cancel {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsRightCancelAdd α] (ha : a ≠ ⊤) (h : b + a = c + a) :
b = c
source
theorem WithTop.add_left_cancel_iff {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsLeftCancelAdd α] (ha : a ≠ ⊤) :
a + b = a + c ↔ b = c
source
theorem WithTop.add_left_cancel {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [IsLeftCancelAdd α] (ha : a ≠ ⊤) (h : a + b = a + c) :
b = c
source
instance WithTop.covariantClass_add_le {α : Type u} [Add α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] :
CovariantClass (WithTop α) (WithTop α) (fun (x1 x2 : WithTop α) => x1 + x2) fun (x1 x2 : WithTop α) => x1 ≤ x2
Equations
  • ⋯ = ⋯
source
instance WithTop.covariantClass_swap_add_le {α : Type u} [Add α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] :
CovariantClass (WithTop α) (WithTop α) (Function.swap fun (x1 x2 : WithTop α) => x1 + x2) fun (x1 x2 : WithTop α) => x1 ≤ x2
Equations
  • ⋯ = ⋯
source
instance WithTop.contravariantClass_add_lt {α : Type u} [Add α] [LT α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] :
ContravariantClass (WithTop α) (WithTop α) (fun (x1 x2 : WithTop α) => x1 + x2) fun (x1 x2 : WithTop α) => x1 < x2
Equations
  • ⋯ = ⋯
source
instance WithTop.contravariantClass_swap_add_lt {α : Type u} [Add α] [LT α] [ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] :
ContravariantClass (WithTop α) (WithTop α) (Function.swap fun (x1 x2 : WithTop α) => x1 + x2) fun (x1 x2 : WithTop α) => x1 < x2
Equations
  • ⋯ = ⋯
source
theorem WithTop.le_of_add_le_add_left {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LE α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (ha : a ≠ ⊤) (h : a + b ≤ a + c) :
b ≤ c
source
theorem WithTop.le_of_add_le_add_right {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LE α] [ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (ha : a ≠ ⊤) (h : b + a ≤ c + a) :
b ≤ c
source
theorem WithTop.add_lt_add_left {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (ha : a ≠ ⊤) (h : b < c) :
a + b < a + c
source
theorem WithTop.add_lt_add_right {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (ha : a ≠ ⊤) (h : b < c) :
b + a < c + a
source
theorem WithTop.add_le_add_iff_left {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (ha : a ≠ ⊤) :
a + b ≤ a + c ↔ b ≤ c
source
theorem WithTop.add_le_add_iff_right {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (ha : a ≠ ⊤) :
b + a ≤ c + a ↔ b ≤ c
source
theorem WithTop.add_lt_add_iff_left {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (ha : a ≠ ⊤) :
a + b < a + c ↔ b < c
source
theorem WithTop.add_lt_add_iff_right {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (ha : a ≠ ⊤) :
b + a < c + a ↔ b < c
source
theorem WithTop.add_lt_add_of_le_of_lt {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} {d : WithTop α} [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (ha : a ≠ ⊤) (hab : a ≤ b) (hcd : c < d) :
a + c < b + d
source
theorem WithTop.add_lt_add_of_lt_of_le {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} {d : WithTop α} [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (hc : c ≠ ⊤) (hab : a < b) (hcd : c ≤ d) :
a + c < b + d
source
@[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
source
instance WithTop.addSemigroup {α : Type u} [AddSemigroup α] :
AddSemigroup (WithTop α)
Equations
source
instance WithTop.addCommSemigroup {α : Type u} [AddCommSemigroup α] :
AddCommSemigroup (WithTop α)
Equations
source
instance WithTop.addZeroClass {α : Type u} [AddZeroClass α] :
AddZeroClass (WithTop α)
Equations
source
instance WithTop.addMonoid {α : Type u} [AddMonoid α] :
AddMonoid (WithTop α)
Equations
  • WithTop.addMonoid = AddMonoid.mk ⋯ ⋯ (fun (n : ℕ) (a : WithTop α) => match a, n with | some a, n => ↑(n • a) | none, 0 => 0 | none, _n.succ => ⊤) ⋯ ⋯
source
@[simp]
theorem WithTop.coe_nsmul {α : Type u} [AddMonoid α] (a : α) (n : ℕ) :
↑(n • a) = n • ↑a
source
def WithTop.addHom {α : Type u} [AddMonoid α] :
α →+ WithTop α

Coercion from α to WithTop α as an AddMonoidHom.

Equations
  • WithTop.addHom = { toFun := WithTop.some, map_zero' := ⋯, map_add' := ⋯ }
Instances For
    source
    @[simp]
    theorem WithTop.coe_addHom {α : Type u} [AddMonoid α] :
    ⇑WithTop.addHom = WithTop.some
    source
    instance WithTop.addCommMonoid {α : Type u} [AddCommMonoid α] :
    AddCommMonoid (WithTop α)
    Equations
    source
    instance WithTop.addMonoidWithOne {α : Type u} [AddMonoidWithOne α] :
    AddMonoidWithOne (WithTop α)
    Equations
    source
    @[simp]
    theorem WithTop.coe_natCast {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
    ↑↑n = ↑n
    source
    @[simp]
    theorem WithTop.top_ne_natCast {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
    ⊤ ≠ ↑n
    source
    @[simp]
    theorem WithTop.natCast_ne_top {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
    ↑n ≠ ⊤
    source
    @[simp]
    theorem WithTop.natCast_lt_top {α : Type u} [AddMonoidWithOne α] [LT α] (n : ℕ) :
    ↑n < ⊤
    source
    @[deprecated WithTop.coe_natCast]
    theorem WithTop.coe_nat {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
    ↑↑n = ↑n

    Alias of WithTop.coe_natCast.

    source
    @[deprecated WithTop.natCast_ne_top]
    theorem WithTop.nat_ne_top {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
    ↑n ≠ ⊤

    Alias of WithTop.natCast_ne_top.

    source
    @[deprecated WithTop.top_ne_natCast]
    theorem WithTop.top_ne_nat {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
    ⊤ ≠ ↑n

    Alias of WithTop.top_ne_natCast.

    source
    @[simp]
    theorem WithTop.coe_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] :
    ↑(OfNat.ofNat n) = OfNat.ofNat n
    source
    @[simp]
    theorem WithTop.coe_eq_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] (m : α) :
    ↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n
    source
    @[simp]
    theorem WithTop.ofNat_eq_coe {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] (m : α) :
    OfNat.ofNat n = ↑m ↔ OfNat.ofNat n = m
    source
    @[simp]
    theorem WithTop.ofNat_ne_top {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] :
    OfNat.ofNat n ≠ ⊤
    source
    @[simp]
    theorem WithTop.top_ne_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] :
    ⊤ ≠ OfNat.ofNat n
    source
    instance WithTop.charZero {α : Type u} [AddMonoidWithOne α] [CharZero α] :
    CharZero (WithTop α)
    Equations
    • ⋯ = ⋯
    source
    instance WithTop.addCommMonoidWithOne {α : Type u} [AddCommMonoidWithOne α] :
    AddCommMonoidWithOne (WithTop α)
    Equations
    source
    instance WithTop.existsAddOfLE {α : Type u} [LE α] [Add α] [ExistsAddOfLE α] :
    ExistsAddOfLE (WithTop α)
    Equations
    • ⋯ = ⋯
    source
    @[simp]
    theorem WithTop.zero_lt_top {α : Type u} [Zero α] [LT α] :
    0 < ⊤
    source
    theorem WithTop.zero_lt_coe {α : Type u} [Zero α] [LT α] (a : α) :
    0 < ↑a ↔ 0 < a
    source
    def ZeroHom.withTopMap {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) :
    ZeroHom (WithTop M) (WithTop N)

    A version of WithTop.map for ZeroHoms

    Equations
    • f.withTopMap = { toFun := WithTop.map ⇑f, map_zero' := ⋯ }
    Instances For
      source
      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
      source
      @[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
      source
      @[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
      source
      def OneHom.withTopMap {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) :
      OneHom (WithTop M) (WithTop N)

      A version of WithTop.map for OneHoms.

      Equations
      • f.withTopMap = { toFun := WithTop.map ⇑f, map_one' := ⋯ }
      Instances For
        source
        @[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
        source
        def AddHom.withTopMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
        AddHom (WithTop M) (WithTop N)

        A version of WithTop.map for AddHoms.

        Equations
        • f.withTopMap = { toFun := WithTop.map ⇑f, map_add' := ⋯ }
        Instances For
          source
          @[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
          source
          def AddMonoidHom.withTopMap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
          WithTop M →+ WithTop N

          A version of WithTop.map for AddMonoidHoms.

          Equations
          • f.withTopMap = { toFun := WithTop.map ⇑f, map_zero' := ⋯, map_add' := ⋯ }
          Instances For
            source
            instance WithBot.zero {α : Type u} [Zero α] :
            Zero (WithBot α)
            Equations
            • WithBot.zero = WithTop.zero
            source
            instance WithBot.one {α : Type u} [One α] :
            One (WithBot α)
            Equations
            • WithBot.one = WithTop.one
            source
            @[simp]
            theorem WithBot.coe_zero {α : Type u} [Zero α] :
            ↑0 = 0
            source
            @[simp]
            theorem WithBot.coe_one {α : Type u} [One α] :
            ↑1 = 1
            source
            @[simp]
            theorem WithBot.coe_eq_zero {α : Type u} [Zero α] {a : α} :
            ↑a = 0 ↔ a = 0
            source
            @[simp]
            theorem WithBot.coe_eq_one {α : Type u} [One α] {a : α} :
            ↑a = 1 ↔ a = 1
            source
            @[simp]
            theorem WithBot.zero_eq_coe {α : Type u} [Zero α] {a : α} :
            0 = ↑a ↔ a = 0
            source
            @[simp]
            theorem WithBot.one_eq_coe {α : Type u} [One α] {a : α} :
            1 = ↑a ↔ a = 1
            source
            @[simp]
            theorem WithBot.bot_ne_zero {α : Type u} [Zero α] :
            ⊥ ≠ 0
            source
            @[simp]
            theorem WithBot.bot_ne_one {α : Type u} [One α] :
            ⊥ ≠ 1
            source
            @[simp]
            theorem WithBot.zero_ne_bot {α : Type u} [Zero α] :
            0 ≠ ⊥
            source
            @[simp]
            theorem WithBot.one_ne_bot {α : Type u} [One α] :
            1 ≠ ⊥
            source
            @[simp]
            theorem WithBot.unbot_zero {α : Type u} [Zero α] :
            WithBot.unbot 0 ⋯ = 0
            source
            @[simp]
            theorem WithBot.unbot_one {α : Type u} [One α] :
            WithBot.unbot 1 ⋯ = 1
            source
            @[simp]
            theorem WithBot.unbot_zero' {α : Type u} [Zero α] (d : α) :
            WithBot.unbot' d 0 = 0
            source
            @[simp]
            theorem WithBot.unbot_one' {α : Type u} [One α] (d : α) :
            WithBot.unbot' d 1 = 1
            source
            @[simp]
            theorem WithBot.coe_nonneg {α : Type u} [Zero α] {a : α} [LE α] :
            0 ≤ ↑a ↔ 0 ≤ a
            source
            @[simp]
            theorem WithBot.one_le_coe {α : Type u} [One α] {a : α} [LE α] :
            1 ≤ ↑a ↔ 1 ≤ a
            source
            @[simp]
            theorem WithBot.coe_le_zero {α : Type u} [Zero α] {a : α} [LE α] :
            ↑a ≤ 0 ↔ a ≤ 0
            source
            @[simp]
            theorem WithBot.coe_le_one {α : Type u} [One α] {a : α} [LE α] :
            ↑a ≤ 1 ↔ a ≤ 1
            source
            @[simp]
            theorem WithBot.coe_pos {α : Type u} [Zero α] {a : α} [LT α] :
            0 < ↑a ↔ 0 < a
            source
            @[simp]
            theorem WithBot.one_lt_coe {α : Type u} [One α] {a : α} [LT α] :
            1 < ↑a ↔ 1 < a
            source
            @[simp]
            theorem WithBot.coe_lt_zero {α : Type u} [Zero α] {a : α} [LT α] :
            ↑a < 0 ↔ a < 0
            source
            @[simp]
            theorem WithBot.coe_lt_one {α : Type u} [One α] {a : α} [LT α] :
            ↑a < 1 ↔ a < 1
            source
            @[simp]
            theorem WithBot.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : α → β) :
            WithBot.map f 0 = ↑(f 0)
            source
            @[simp]
            theorem WithBot.map_one {α : Type u} [One α] {β : Type u_1} (f : α → β) :
            WithBot.map f 1 = ↑(f 1)
            source
            instance WithBot.zeroLEOneClass {α : Type u} [One α] [Zero α] [LE α] [ZeroLEOneClass α] :
            ZeroLEOneClass (WithBot α)
            Equations
            • ⋯ = ⋯
            source
            instance WithBot.add {α : Type u} [Add α] :
            Add (WithBot α)
            Equations
            • WithBot.add = WithTop.add
            source
            instance WithBot.AddSemigroup {α : Type u} [AddSemigroup α] :
            AddSemigroup (WithBot α)
            Equations
            • WithBot.AddSemigroup = WithTop.addSemigroup
            source
            instance WithBot.addCommSemigroup {α : Type u} [AddCommSemigroup α] :
            AddCommSemigroup (WithBot α)
            Equations
            • WithBot.addCommSemigroup = WithTop.addCommSemigroup
            source
            instance WithBot.addZeroClass {α : Type u} [AddZeroClass α] :
            AddZeroClass (WithBot α)
            Equations
            • WithBot.addZeroClass = WithTop.addZeroClass
            source
            instance WithBot.addMonoid {α : Type u} [AddMonoid α] :
            AddMonoid (WithBot α)
            Equations
            • WithBot.addMonoid = WithTop.addMonoid
            source
            def WithBot.addHom {α : Type u} [AddMonoid α] :
            α →+ WithBot α

            Coercion from α to WithBot α as an AddMonoidHom.

            Equations
            • WithBot.addHom = { toFun := WithTop.some, map_zero' := ⋯, map_add' := ⋯ }
            Instances For
              source
              @[simp]
              theorem WithBot.coe_addHom {α : Type u} [AddMonoid α] :
              ⇑WithBot.addHom = WithBot.some
              source
              @[simp]
              theorem WithBot.coe_nsmul {α : Type u} [AddMonoid α] (a : α) (n : ℕ) :
              ↑(n • a) = n • ↑a
              source
              instance WithBot.addCommMonoid {α : Type u} [AddCommMonoid α] :
              AddCommMonoid (WithBot α)
              Equations
              • WithBot.addCommMonoid = WithTop.addCommMonoid
              source
              instance WithBot.addMonoidWithOne {α : Type u} [AddMonoidWithOne α] :
              AddMonoidWithOne (WithBot α)
              Equations
              • WithBot.addMonoidWithOne = WithTop.addMonoidWithOne
              source
              theorem WithBot.coe_natCast {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
              ↑↑n = ↑n
              source
              @[simp]
              theorem WithBot.natCast_ne_bot {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
              ↑n ≠ ⊥
              source
              @[simp]
              theorem WithBot.bot_ne_natCast {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
              ⊥ ≠ ↑n
              source
              @[deprecated WithBot.coe_natCast]
              theorem WithBot.coe_nat {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
              ↑↑n = ↑n

              Alias of WithBot.coe_natCast.

              source
              @[deprecated WithBot.natCast_ne_bot]
              theorem WithBot.nat_ne_bot {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
              ↑n ≠ ⊥

              Alias of WithBot.natCast_ne_bot.

              source
              @[deprecated WithBot.bot_ne_natCast]
              theorem WithBot.bot_ne_nat {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
              ⊥ ≠ ↑n

              Alias of WithBot.bot_ne_natCast.

              source
              @[simp]
              theorem WithBot.coe_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] :
              ↑(OfNat.ofNat n) = OfNat.ofNat n
              source
              @[simp]
              theorem WithBot.coe_eq_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] (m : α) :
              ↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n
              source
              @[simp]
              theorem WithBot.ofNat_eq_coe {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] (m : α) :
              OfNat.ofNat n = ↑m ↔ OfNat.ofNat n = m
              source
              @[simp]
              theorem WithBot.ofNat_ne_bot {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] :
              OfNat.ofNat n ≠ ⊥
              source
              @[simp]
              theorem WithBot.bot_ne_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] :
              ⊥ ≠ OfNat.ofNat n
              source
              instance WithBot.charZero {α : Type u} [AddMonoidWithOne α] [CharZero α] :
              CharZero (WithBot α)
              Equations
              • ⋯ = ⋯
              source
              instance WithBot.addCommMonoidWithOne {α : Type u} [AddCommMonoidWithOne α] :
              AddCommMonoidWithOne (WithBot α)
              Equations
              • WithBot.addCommMonoidWithOne = WithTop.addCommMonoidWithOne
              source
              @[simp]
              theorem WithBot.coe_add {α : Type u} [Add α] (a : α) (b : α) :
              ↑(a + b) = ↑a + ↑b
              source
              @[simp]
              theorem WithBot.bot_add {α : Type u} [Add α] (a : WithBot α) :
              ⊥ + a = ⊥
              source
              @[simp]
              theorem WithBot.add_bot {α : Type u} [Add α] (a : WithBot α) :
              a + ⊥ = ⊥
              source
              @[simp]
              theorem WithBot.add_eq_bot {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} :
              a + b = ⊥ ↔ a = ⊥ ∨ b = ⊥
              source
              theorem WithBot.add_ne_bot {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} :
              a + b ≠ ⊥ ↔ a ≠ ⊥ ∧ b ≠ ⊥
              source
              theorem WithBot.bot_lt_add {α : Type u} [Add α] [LT α] {a : WithBot α} {b : WithBot α} :
              ⊥ < a + b ↔ ⊥ < a ∧ ⊥ < b
              source
              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
              source
              theorem WithBot.add_coe_eq_bot_iff {α : Type u} [Add α] {a : WithBot α} {y : α} :
              a + ↑y = ⊥ ↔ a = ⊥
              source
              theorem WithBot.coe_add_eq_bot_iff {α : Type u} [Add α] {b : WithBot α} {x : α} :
              ↑x + b = ⊥ ↔ b = ⊥
              source
              theorem WithBot.add_right_cancel_iff {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsRightCancelAdd α] (ha : a ≠ ⊥) :
              b + a = c + a ↔ b = c
              source
              theorem WithBot.add_right_cancel {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsRightCancelAdd α] (ha : a ≠ ⊥) (h : b + a = c + a) :
              b = c
              source
              theorem WithBot.add_left_cancel_iff {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsLeftCancelAdd α] (ha : a ≠ ⊥) :
              a + b = a + c ↔ b = c
              source
              theorem WithBot.add_left_cancel {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [IsLeftCancelAdd α] (ha : a ≠ ⊥) (h : a + b = a + c) :
              b = c
              source
              @[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
              source
              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
              source
              def ZeroHom.withBotMap {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) :
              ZeroHom (WithBot M) (WithBot N)

              A version of WithBot.map for ZeroHoms

              Equations
              • f.withBotMap = { toFun := WithBot.map ⇑f, map_zero' := ⋯ }
              Instances For
                source
                @[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
                source
                @[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
                source
                def OneHom.withBotMap {M : Type u_1} {N : Type u_2} [One M] [One N] (f : OneHom M N) :
                OneHom (WithBot M) (WithBot N)

                A version of WithBot.map for OneHoms.

                Equations
                • f.withBotMap = { toFun := WithBot.map ⇑f, map_one' := ⋯ }
                Instances For
                  source
                  @[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
                  source
                  def AddHom.withBotMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
                  AddHom (WithBot M) (WithBot N)

                  A version of WithBot.map for AddHoms.

                  Equations
                  • f.withBotMap = { toFun := WithBot.map ⇑f, map_add' := ⋯ }
                  Instances For
                    source
                    @[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
                    source
                    def AddMonoidHom.withBotMap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                    WithBot M →+ WithBot N

                    A version of WithBot.map for AddMonoidHoms.

                    Equations
                    • f.withBotMap = { toFun := WithBot.map ⇑f, map_zero' := ⋯, map_add' := ⋯ }
                    Instances For
                      source
                      instance WithBot.covariantClass_add_le {α : Type u} [Add α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] :
                      CovariantClass (WithBot α) (WithBot α) (fun (x1 x2 : WithBot α) => x1 + x2) fun (x1 x2 : WithBot α) => x1 ≤ x2
                      Equations
                      • ⋯ = ⋯
                      source
                      instance WithBot.covariantClass_swap_add_le {α : Type u} [Add α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] :
                      CovariantClass (WithBot α) (WithBot α) (Function.swap fun (x1 x2 : WithBot α) => x1 + x2) fun (x1 x2 : WithBot α) => x1 ≤ x2
                      Equations
                      • ⋯ = ⋯
                      source
                      instance WithBot.contravariantClass_add_lt {α : Type u} [Add α] [Preorder α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] :
                      ContravariantClass (WithBot α) (WithBot α) (fun (x1 x2 : WithBot α) => x1 + x2) fun (x1 x2 : WithBot α) => x1 < x2
                      Equations
                      • ⋯ = ⋯
                      source
                      instance WithBot.contravariantClass_swap_add_lt {α : Type u} [Add α] [Preorder α] [ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] :
                      ContravariantClass (WithBot α) (WithBot α) (Function.swap fun (x1 x2 : WithBot α) => x1 + x2) fun (x1 x2 : WithBot α) => x1 < x2
                      Equations
                      • ⋯ = ⋯
                      source
                      theorem WithBot.le_of_add_le_add_left {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (ha : a ≠ ⊥) (h : a + b ≤ a + c) :
                      b ≤ c
                      source
                      theorem WithBot.le_of_add_le_add_right {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (ha : a ≠ ⊥) (h : b + a ≤ c + a) :
                      b ≤ c
                      source
                      theorem WithBot.add_lt_add_left {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (ha : a ≠ ⊥) (h : b < c) :
                      a + b < a + c
                      source
                      theorem WithBot.add_lt_add_right {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (ha : a ≠ ⊥) (h : b < c) :
                      b + a < c + a
                      source
                      theorem WithBot.add_le_add_iff_left {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (ha : a ≠ ⊥) :
                      a + b ≤ a + c ↔ b ≤ c
                      source
                      theorem WithBot.add_le_add_iff_right {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (ha : a ≠ ⊥) :
                      b + a ≤ c + a ↔ b ≤ c
                      source
                      theorem WithBot.add_lt_add_iff_left {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (ha : a ≠ ⊥) :
                      a + b < a + c ↔ b < c
                      source
                      theorem WithBot.add_lt_add_iff_right {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (ha : a ≠ ⊥) :
                      b + a < c + a ↔ b < c
                      source
                      theorem WithBot.add_lt_add_of_le_of_lt {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} {d : WithBot α} [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (hb : b ≠ ⊥) (hab : a ≤ b) (hcd : c < d) :
                      a + c < b + d
                      source
                      theorem WithBot.add_lt_add_of_lt_of_le {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} {d : WithBot α} [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (hd : d ≠ ⊥) (hab : a < b) (hcd : c ≤ d) :
                      a + c < b + d