Adjoining top/bottom elements to ordered monoids.

@[implicit_reducible]

instance WithTop.one {α : Type u} [One α] : One (WithTop α)

@[implicit_reducible]

instance WithTop.zero {α : Type u} [Zero α] : Zero (WithTop α)

@[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

theorem WithTop.coe_ne_one {α : Type u} [One α] {a : α} : ↑a ≠ 1 ↔ a ≠ 1

theorem WithTop.coe_ne_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 α] : ⊤ ≠ 1

@[simp]

theorem WithTop.top_ne_zero {α : Type u} [Zero α] : ⊤ ≠ 0

@[simp]

theorem WithTop.one_ne_top {α : Type u} [One α] : 1 ≠ ⊤

@[simp]

theorem WithTop.zero_ne_top {α : Type u} [Zero α] : 0 ≠ ⊤

@[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

@[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 α] : ZeroLEOneClass (WithTop α)

@[implicit_reducible]

instance WithTop.add {α : Type u} [Add α] : Add (WithTop α)

@[simp]

theorem WithTop.coe_add {α : Type u} [Add α] (a b : α) : ↑(a + b) = ↑a + ↑b

@[simp]

theorem WithTop.top_add {α : Type u} [Add α] (x : WithTop α) : ⊤ + x = ⊤

@[simp]

theorem WithTop.add_top {α : Type u} [Add α] (x : WithTop α) : x + ⊤ = ⊤

@[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 α} : x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

@[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 IsAddLeftRegular.withTop {α : Type u} [Add α] {a : α} (ha : IsAddLeftRegular a) : IsAddLeftRegular ↑a

theorem IsAddRightRegular.withTop {α : Type u} [Add α] {a : α} (ha : IsAddRightRegular a) : IsAddRightRegular ↑a

theorem AddLECancellable.withTop {α : Type u} [Add α] {a : α} [LE α] (ha : AddLECancellable a) : AddLECancellable ↑a

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

instance WithTop.addLeftMono {α : Type u} [Add α] [LE α] [AddLeftMono α] : AddLeftMono (WithTop α)

instance WithTop.addRightMono {α : Type u} [Add α] [LE α] [AddRightMono α] : AddRightMono (WithTop α)

instance WithTop.addLeftReflectLT {α : Type u} [Add α] [LT α] [AddLeftReflectLT α] : AddLeftReflectLT (WithTop α)

instance WithTop.addRightReflectLT {α : Type u} [Add α] [LT α] [AddRightReflectLT α] : AddRightReflectLT (WithTop α)

theorem WithTop.le_of_add_le_add_left {α : Type u} [Add α] {x y z : WithTop α} [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊤) : x + y ≤ x + z → y ≤ z

theorem WithTop.le_of_add_le_add_right {α : Type u} [Add α] {x y z : WithTop α} [LE α] [AddRightReflectLE α] (hz : z ≠ ⊤) : x + z ≤ y + z → x ≤ y

theorem WithTop.add_lt_add_left {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddLeftStrictMono α] (hx : x ≠ ⊤) : y < z → x + y < x + z

theorem WithTop.add_lt_add_right {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddRightStrictMono α] (hz : z ≠ ⊤) : x < y → x + z < y + z

theorem WithTop.add_lt_add {α : Type u} [Add α] {w x y z : WithTop α} [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] (xz : x < z) (yw : y < w) : x + y < z + w

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 α] [AddLeftReflectLE α] (hx : x ≠ ⊤) : AddLECancellable x

theorem WithTop.addLECancellable_of_lt_top {α : Type u} [Add α] {x : WithTop α} [Preorder α] [AddLeftReflectLE α] (hx : x < ⊤) : AddLECancellable x

theorem WithTop.addLECancellable_coe {α : Type u} [Add α] [LE α] [AddLeftReflectLE α] (a : α) : AddLECancellable ↑a

theorem WithTop.addLECancellable_iff_ne_top {α : Type u} [Add α] {x : WithTop α} [Nonempty α] [Preorder α] [AddLeftReflectLE α] : AddLECancellable x ↔ x ≠ ⊤

@[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

@[implicit_reducible]

instance WithTop.addSemigroup {α : Type u} [AddSemigroup α] : AddSemigroup (WithTop α)

@[implicit_reducible]

instance WithTop.addCommSemigroup {α : Type u} [AddCommSemigroup α] : AddCommSemigroup (WithTop α)

@[implicit_reducible]

instance WithTop.addZeroClass {α : Type u} [AddZeroClass α] : AddZeroClass (WithTop α)

@[implicit_reducible]

instance WithTop.addMonoid {α : Type u} [AddMonoid α] : AddMonoid (WithTop α)

@[simp]

theorem WithTop.coe_nsmul {α : Type u} [AddMonoid α] (a : α) (n : ℕ) : ↑(n • a) = n • ↑a

def WithTop.addHom {α : Type u} [AddMonoid α] : α →+ WithTop α

Coercion from α to WithTop α as an AddMonoidHom.

@[simp]

theorem WithTop.coe_addHom {α : Type u} [AddMonoid α] : ⇑addHom = some

@[implicit_reducible]

instance WithTop.addCommMonoid {α : Type u} [AddCommMonoid α] : AddCommMonoid (WithTop α)

@[implicit_reducible]

instance WithTop.natCast {α : Type u} [NatCast α] : NatCast (WithTop α)

@[implicit_reducible]

instance WithTop.addMonoidWithOne {α : Type u} [AddMonoidWithOne α] : AddMonoidWithOne (WithTop α)

@[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] : ↑(OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem WithTop.coe_eq_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] (m : α) : ↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n

@[simp]

theorem WithTop.ofNat_eq_coe {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] (m : α) : OfNat.ofNat n = ↑m ↔ OfNat.ofNat n = m

@[simp]

theorem WithTop.ofNat_ne_top {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n ≠ ⊤

@[simp]

theorem WithTop.top_ne_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] : ⊤ ≠ OfNat.ofNat n

@[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

instance WithTop.charZero {α : Type u} [AddMonoidWithOne α] [CharZero α] : CharZero (WithTop α)

@[implicit_reducible]

instance WithTop.addCommMonoidWithOne {α : Type u} [AddCommMonoidWithOne α] : AddCommMonoidWithOne (WithTop α)

instance WithTop.existsAddOfLE {α : Type u} [LE α] [Add α] [ExistsAddOfLE α] : ExistsAddOfLE (WithTop α)

@[simp]

theorem WithTop.one_lt_top {α : Type u} [One α] [LT α] : 1 < ⊤

@[simp]

theorem WithTop.top_pos {α : Type u} [Zero α] [LT α] : 0 < ⊤

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.

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

@[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 AddHom.withTopMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) : WithTop M →ₙ+ WithTop N

A version of WithTop.map for AddHoms.

@[simp]

theorem AddHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [Add M] [Add 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) : WithTop M →+ WithTop N

A version of WithTop.map for AddMonoidHoms.

@[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

@[implicit_reducible]

instance WithBot.one {α : Type u} [One α] : One (WithBot α)

@[implicit_reducible]

instance WithBot.zero {α : Type u} [Zero α] : Zero (WithBot α)

@[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 α] : ⊥ ≠ 1

@[simp]

theorem WithBot.bot_ne_zero {α : Type u} [Zero α] : ⊥ ≠ 0

@[simp]

theorem WithBot.one_ne_bot {α : Type u} [One α] : 1 ≠ ⊥

@[simp]

theorem WithBot.zero_ne_bot {α : Type u} [Zero α] : 0 ≠ ⊥

@[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

@[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.bot_lt_one {α : Type u} [One α] [LT α] : ⊥ < 1

@[simp]

theorem WithBot.bot_neg {α : Type u} [Zero α] [LT α] : ⊥ < 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 α] : ZeroLEOneClass (WithBot α)

@[implicit_reducible]

instance WithBot.add {α : Type u} [Add α] : Add (WithBot α)

@[simp]

theorem WithBot.coe_add {α : Type u} [Add α] (a b : α) : ↑(a + b) = ↑a + ↑b

@[simp]

theorem WithBot.bot_add {α : Type u} [Add α] (x : WithBot α) : ⊥ + x = ⊥

@[simp]

theorem WithBot.add_bot {α : Type u} [Add α] (x : WithBot α) : x + ⊥ = ⊥

@[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 α} : x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥

@[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 IsAddLeftRegular.withBot {α : Type u} [Add α] {a : α} (ha : IsAddLeftRegular a) : IsAddLeftRegular ↑a

theorem IsAddRightRegular.withBot {α : Type u} [Add α] {a : α} (ha : IsAddRightRegular a) : IsAddRightRegular ↑a

theorem AddLECancellable.withBot {α : Type u} [Add α] {a : α} [LE α] (ha : AddLECancellable a) : AddLECancellable ↑a

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

instance WithBot.addLeftMono {α : Type u} [Add α] [LE α] [AddLeftMono α] : AddLeftMono (WithBot α)

instance WithBot.addRightMono {α : Type u} [Add α] [LE α] [AddRightMono α] : AddRightMono (WithBot α)

instance WithBot.addLeftReflectLT {α : Type u} [Add α] [LT α] [AddLeftReflectLT α] : AddLeftReflectLT (WithBot α)

instance WithBot.addRightReflectLT {α : Type u} [Add α] [LT α] [AddRightReflectLT α] : AddRightReflectLT (WithBot α)

theorem WithBot.le_of_add_le_add_left {α : Type u} [Add α] {x y z : WithBot α} [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊥) : x + y ≤ x + z → y ≤ z

theorem WithBot.le_of_add_le_add_right {α : Type u} [Add α] {x y z : WithBot α} [LE α] [AddRightReflectLE α] (hz : z ≠ ⊥) : x + z ≤ y + z → x ≤ y

theorem WithBot.add_lt_add_left {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddLeftStrictMono α] (hx : x ≠ ⊥) : y < z → x + y < x + z

theorem WithBot.add_lt_add_right {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddRightStrictMono α] (hz : z ≠ ⊥) : x < y → x + 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 α] [AddLeftReflectLE α] (hx : x ≠ ⊥) : AddLECancellable x

theorem WithBot.addLECancellable_of_lt_bot {α : Type u} [Add α] {x : WithBot α} [Preorder α] [AddLeftReflectLE α] (hx : x < ⊥) : AddLECancellable x

theorem WithBot.addLECancellable_coe {α : Type u} [Add α] [LE α] [AddLeftReflectLE α] (a : α) : AddLECancellable ↑a

theorem WithBot.addLECancellable_iff_ne_bot {α : Type u} [Add α] {x : WithBot α} [Nonempty α] [Preorder α] [AddLeftReflectLE α] : AddLECancellable x ↔ x ≠ ⊥

theorem WithBot.add_le_add_iff_right' {α : Type u_1} [Add α] [LE α] [AddRightMono α] [AddRightReflectLE α] {a b c : WithBot (WithTop α)} (hc : c ≠ ⊥) (hc' : c ≠ ⊤) : a + c ≤ b + c ↔ a ≤ b

Addition in WithBot (WithTop α) is right cancellative provided the element being cancelled is not ⊤ or ⊥.

@[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

@[implicit_reducible]

instance WithBot.addSemigroup {α : Type u} [AddSemigroup α] : AddSemigroup (WithBot α)

@[implicit_reducible]

instance WithBot.addCommSemigroup {α : Type u} [AddCommSemigroup α] : AddCommSemigroup (WithBot α)

@[implicit_reducible]

instance WithBot.addZeroClass {α : Type u} [AddZeroClass α] : AddZeroClass (WithBot α)

@[implicit_reducible]

instance WithBot.addMonoid {α : Type u} [AddMonoid α] : AddMonoid (WithBot α)

def WithBot.addHom {α : Type u} [AddMonoid α] : α →+ WithBot α

Coercion from α to WithBot α as an AddMonoidHom.

@[simp]

theorem WithBot.coe_addHom {α : Type u} [AddMonoid α] : ⇑addHom = some

@[simp]

theorem WithBot.coe_nsmul {α : Type u} [AddMonoid α] (a : α) (n : ℕ) : ↑(n • a) = n • ↑a

@[implicit_reducible]

instance WithBot.addCommMonoid {α : Type u} [AddCommMonoid α] : AddCommMonoid (WithBot α)

@[implicit_reducible]

instance WithBot.natCast {α : Type u} [NatCast α] : NatCast (WithBot α)

@[implicit_reducible]

instance WithBot.addMonoidWithOne {α : Type u} [AddMonoidWithOne α] : AddMonoidWithOne (WithBot α)

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] : ↑(OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem WithBot.coe_eq_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] (m : α) : ↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n

@[simp]

theorem WithBot.ofNat_eq_coe {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] (m : α) : OfNat.ofNat n = ↑m ↔ OfNat.ofNat n = m

@[simp]

theorem WithBot.ofNat_ne_bot {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n ≠ ⊥

@[simp]

theorem WithBot.bot_ne_ofNat {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] : ⊥ ≠ OfNat.ofNat n

@[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

@[simp]

theorem WithBot.bot_lt_natCast {α : Type u} [AddMonoidWithOne α] [LT α] (n : ℕ) : ⊥ < ↑n

instance WithBot.charZero {α : Type u} [AddMonoidWithOne α] [CharZero α] : CharZero (WithBot α)

@[implicit_reducible]

instance WithBot.addCommMonoidWithOne {α : Type u} [AddCommMonoidWithOne α] : AddCommMonoidWithOne (WithBot α)

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.

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

@[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

@[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

def AddHom.withBotMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) : WithBot M →ₙ+ WithBot N

A version of WithBot.map for AddHoms.

@[simp]

theorem AddHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [Add M] [Add 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) : WithBot M →+ WithBot N

A version of WithBot.map for AddMonoidHoms.

@[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