Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Adjoining top/bottom elements to ordered monoids. #

source
instance WithTop.one {α : Type u} [One α] :
One (WithTop α)
Equations
  • WithTop.one = { one := ↑1 }
source
instance WithTop.zero {α : Type u} [Zero α] :
Zero (WithTop α)
Equations
  • WithTop.zero = { zero := ↑0 }
source
@[simp]
theorem WithTop.coe_one {α : Type u} [One α] :
↑1 = 1
source
@[simp]
theorem WithTop.coe_zero {α : Type u} [Zero α] :
↑0 = 0
source
@[simp]
theorem WithTop.coe_eq_one {α : Type u} [One α] {a : α} :
↑a = 1 ↔ a = 1
source
@[simp]
theorem WithTop.coe_eq_zero {α : Type u} [Zero α] {a : α} :
↑a = 0 ↔ a = 0
source
@[simp]
theorem WithTop.one_eq_coe {α : Type u} [One α] {a : α} :
1 = ↑a ↔ a = 1
source
@[simp]
theorem WithTop.zero_eq_coe {α : Type u} [Zero α] {a : α} :
0 = ↑a ↔ a = 0
source
@[simp]
theorem WithTop.top_ne_one {α : Type u} [One α] :
⊤ ≠ 1
source
@[simp]
theorem WithTop.top_ne_zero {α : Type u} [Zero α] :
⊤ ≠ 0
source
@[simp]
theorem WithTop.one_ne_top {α : Type u} [One α] :
1 ≠ ⊤
source
@[simp]
theorem WithTop.zero_ne_top {α : Type u} [Zero α] :
0 ≠ ⊤
source
@[simp]
theorem WithTop.untop_one {α : Type u} [One α] :
WithTop.untop 1 ⋯ = 1
source
@[simp]
theorem WithTop.untop_zero {α : Type u} [Zero α] :
WithTop.untop 0 ⋯ = 0
source
@[simp]
theorem WithTop.untop_one' {α : Type u} [One α] (d : α) :
WithTop.untop' d 1 = 1
source
@[simp]
theorem WithTop.untop_zero' {α : Type u} [Zero α] (d : α) :
WithTop.untop' d 0 = 0
source
@[simp]
theorem WithTop.one_le_coe {α : Type u} [One α] [LE α] {a : α} :
1 ≤ ↑a ↔ 1 ≤ a
source
@[simp]
theorem WithTop.coe_nonneg {α : Type u} [Zero α] [LE α] {a : α} :
0 ≤ ↑a ↔ 0 ≤ a
source
@[simp]
theorem WithTop.coe_le_one {α : Type u} [One α] [LE α] {a : α} :
↑a ≤ 1 ↔ a ≤ 1
source
@[simp]
theorem WithTop.coe_le_zero {α : Type u} [Zero α] [LE α] {a : α} :
↑a ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem WithTop.one_lt_coe {α : Type u} [One α] [LT α] {a : α} :
1 < ↑a ↔ 1 < a
source
@[simp]
theorem WithTop.coe_pos {α : Type u} [Zero α] [LT α] {a : α} :
0 < ↑a ↔ 0 < a
source
@[simp]
theorem WithTop.coe_lt_one {α : Type u} [One α] [LT α] {a : α} :
↑a < 1 ↔ a < 1
source
@[simp]
theorem WithTop.coe_lt_zero {α : Type u} [Zero α] [LT α] {a : α} :
↑a < 0 ↔ a < 0
source
@[simp]
theorem WithTop.map_one {α : Type u} [One α] {β : Type u_1} (f : α → β) :
WithTop.map f 1 = ↑(f 1)
source
@[simp]
theorem WithTop.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : α → β) :
WithTop.map f 0 = ↑(f 0)
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.addLeftMono {α : Type u} [Add α] [LE α] [AddLeftMono α] :
AddLeftMono (WithTop α)
Equations
  • ⋯ = ⋯
source
instance WithTop.addRightMono {α : Type u} [Add α] [LE α] [AddRightMono α] :
AddRightMono (WithTop α)
Equations
  • ⋯ = ⋯
source
instance WithTop.addLeftReflectLT {α : Type u} [Add α] [LT α] [AddLeftReflectLT α] :
AddLeftReflectLT (WithTop α)
Equations
  • ⋯ = ⋯
source
instance WithTop.addRightReflectLT {α : Type u} [Add α] [LT α] [AddRightReflectLT α] :
AddRightReflectLT (WithTop α)
Equations
  • ⋯ = ⋯
source
theorem WithTop.le_of_add_le_add_left {α : Type u} [Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [LE α] [AddLeftReflectLE α] (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 α] [AddRightReflectLE α] (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 α] [AddLeftStrictMono α] (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 α] [AddRightStrictMono α] (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 α] [AddLeftMono α] [AddLeftReflectLE α] (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 α] [AddRightMono α] [AddRightReflectLE α] (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 α] [AddLeftStrictMono α] [AddLeftReflectLT α] (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 α] [AddRightStrictMono α] [AddRightReflectLT α] (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 α] [AddLeftStrictMono α] [AddRightMono α] (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 α] [AddLeftMono α] [AddRightStrictMono α] (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' := ⋯ }
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.one_lt_top {α : Type u} [One α] [LT α] :
1 < ⊤
source
@[simp]
theorem WithTop.top_pos {α : Type u} [Zero α] [LT α] :
0 < ⊤
source
@[deprecated WithTop.top_pos]
theorem WithTop.zero_lt_top {α : Type u} [Zero α] [LT α] :
0 < ⊤

Alias of WithTop.top_pos.

source
@[deprecated WithTop.coe_pos]
theorem WithTop.zero_lt_coe {α : Type u} [Zero α] [LT α] (a : α) :
0 < ↑a ↔ 0 < a
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' := ⋯ }
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' := ⋯ }
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 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' := ⋯ }
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 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' := ⋯ }
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
instance WithBot.one {α : Type u} [One α] :
One (WithBot α)
Equations
  • WithBot.one = WithTop.one
source
instance WithBot.zero {α : Type u} [Zero α] :
Zero (WithBot α)
Equations
  • WithBot.zero = WithTop.zero
source
@[simp]
theorem WithBot.coe_one {α : Type u} [One α] :
↑1 = 1
source
@[simp]
theorem WithBot.coe_zero {α : Type u} [Zero α] :
↑0 = 0
source
@[simp]
theorem WithBot.coe_eq_one {α : Type u} [One α] {a : α} :
↑a = 1 ↔ a = 1
source
@[simp]
theorem WithBot.coe_eq_zero {α : Type u} [Zero α] {a : α} :
↑a = 0 ↔ a = 0
source
@[simp]
theorem WithBot.one_eq_coe {α : Type u} [One α] {a : α} :
1 = ↑a ↔ a = 1
source
@[simp]
theorem WithBot.zero_eq_coe {α : Type u} [Zero α] {a : α} :
0 = ↑a ↔ a = 0
source
@[simp]
theorem WithBot.bot_ne_one {α : Type u} [One α] :
⊥ ≠ 1
source
@[simp]
theorem WithBot.bot_ne_zero {α : Type u} [Zero α] :
⊥ ≠ 0
source
@[simp]
theorem WithBot.one_ne_bot {α : Type u} [One α] :
1 ≠ ⊥
source
@[simp]
theorem WithBot.zero_ne_bot {α : Type u} [Zero α] :
0 ≠ ⊥
source
@[simp]
theorem WithBot.unbot_one {α : Type u} [One α] :
WithBot.unbot 1 ⋯ = 1
source
@[simp]
theorem WithBot.unbot_zero {α : Type u} [Zero α] :
WithBot.unbot 0 ⋯ = 0
source
@[simp]
theorem WithBot.unbot_one' {α : Type u} [One α] (d : α) :
WithBot.unbot' d 1 = 1
source
@[simp]
theorem WithBot.unbot_zero' {α : Type u} [Zero α] (d : α) :
WithBot.unbot' d 0 = 0
source
@[simp]
theorem WithBot.one_le_coe {α : Type u} [One α] {a : α} [LE α] :
1 ≤ ↑a ↔ 1 ≤ a
source
@[simp]
theorem WithBot.coe_nonneg {α : Type u} [Zero α] {a : α} [LE α] :
0 ≤ ↑a ↔ 0 ≤ a
source
@[simp]
theorem WithBot.coe_le_one {α : Type u} [One α] {a : α} [LE α] :
↑a ≤ 1 ↔ a ≤ 1
source
@[simp]
theorem WithBot.coe_le_zero {α : Type u} [Zero α] {a : α} [LE α] :
↑a ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem WithBot.one_lt_coe {α : Type u} [One α] {a : α} [LT α] :
1 < ↑a ↔ 1 < a
source
@[simp]
theorem WithBot.coe_pos {α : Type u} [Zero α] {a : α} [LT α] :
0 < ↑a ↔ 0 < a
source
@[simp]
theorem WithBot.coe_lt_one {α : Type u} [One α] {a : α} [LT α] :
↑a < 1 ↔ a < 1
source
@[simp]
theorem WithBot.coe_lt_zero {α : Type u} [Zero α] {a : α} [LT α] :
↑a < 0 ↔ a < 0
source
@[simp]
theorem WithBot.map_one {α : Type u} [One α] {β : Type u_1} (f : α → β) :
WithBot.map f 1 = ↑(f 1)
source
@[simp]
theorem WithBot.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : α → β) :
WithBot.map f 0 = ↑(f 0)
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' := ⋯ }
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
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' := ⋯ }
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' := ⋯ }
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 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' := ⋯ }
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 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' := ⋯ }
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
instance WithBot.addLeftMono {α : Type u} [Add α] [Preorder α] [AddLeftMono α] :
AddLeftMono (WithBot α)
Equations
  • ⋯ = ⋯
source
instance WithBot.addRightMono {α : Type u} [Add α] [Preorder α] [AddRightMono α] :
AddRightMono (WithBot α)
Equations
  • ⋯ = ⋯
source
instance WithBot.addLeftReflectLT {α : Type u} [Add α] [Preorder α] [AddLeftReflectLT α] :
AddLeftReflectLT (WithBot α)
Equations
  • ⋯ = ⋯
source
instance WithBot.addRightReflectLT {α : Type u} [Add α] [Preorder α] [AddRightReflectLT α] :
AddRightReflectLT (WithBot α)
Equations
  • ⋯ = ⋯
source
theorem WithBot.le_of_add_le_add_left {α : Type u} [Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [Preorder α] [AddLeftReflectLE α] (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 α] [AddRightReflectLE α] (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 α] [AddLeftStrictMono α] (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 α] [AddRightStrictMono α] (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 α] [AddLeftMono α] [AddLeftReflectLE α] (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 α] [AddRightMono α] [AddRightReflectLE α] (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 α] [AddLeftStrictMono α] [AddLeftReflectLT α] (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 α] [AddRightStrictMono α] [AddRightReflectLT α] (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 α] [AddLeftStrictMono α] [AddRightMono α] (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 α] [AddLeftMono α] [AddRightStrictMono α] (hd : d ≠ ⊥) (hab : a < b) (hcd : c ≤ d) :
a + c < b + d