# 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
theorem WithTop.coe_ne_one {α : Type u} [One α] {a : α} :
↑a ≠ 1 ↔ a ≠ 1
source
theorem WithTop.coe_ne_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 α] :
untop 1 ⋯ = 1
source
@[simp]
theorem WithTop.untop_zero {α : Type u} [Zero α] :
untop 0 ⋯ = 0
source
@[simp]
theorem WithTop.untopD_one {α : Type u} [One α] (d : α) :
untopD d 1 = 1
source
@[simp]
theorem WithTop.untopD_zero {α : Type u} [Zero α] (d : α) :
untopD 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 : α → β) :
map f 1 = ↑(f 1)
source
@[simp]
theorem WithTop.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : α → β) :
map f 0 = ↑(f 0)
source
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
source
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
source
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
source
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
source
instance WithTop.zeroLEOneClass {α : Type u} [One α] [Zero α] [LE α] [ZeroLEOneClass α] :
ZeroLEOneClass (WithTop α)
source
instance WithTop.add {α : Type u} [Add α] :
Add (WithTop α)
Equations

- WithTop.add = { add := Option.map₂ fun (x1 x2 : α) => x1 + x2 }

source
@[simp]
theorem WithTop.coe_add {α : Type u} [Add α] (a b : α) :
↑(a + b) = ↑a + ↑b
source
@[simp]
theorem WithTop.top_add {α : Type u} [Add α] (x : WithTop α) :
⊤ + x = ⊤
source
@[simp]
theorem WithTop.add_top {α : Type u} [Add α] (x : WithTop α) :
x + ⊤ = ⊤
source
@[simp]
theorem WithTop.add_eq_top {α : Type u} [Add α] {x y : WithTop α} :
x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤
source
theorem WithTop.add_ne_top {α : Type u} [Add α] {x y : WithTop α} :
x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤
source
@[simp]
theorem WithTop.add_lt_top {α : Type u} [Add α] {x y : WithTop α} [LT α] :
x + y < ⊤ ↔ x < ⊤ ∧ y < ⊤
source
theorem WithTop.add_eq_coe {α : Type u} [Add α] {a 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 α} {b : α} :
x + ↑b = ⊤ ↔ x = ⊤
source
theorem WithTop.coe_add_eq_top_iff {α : Type u} [Add α] {y : WithTop α} {a : α} :
↑a + y = ⊤ ↔ y = ⊤
source
theorem WithTop.add_right_inj {α : Type u} [Add α] {x y z : WithTop α} [IsRightCancelAdd α] (hz : z ≠ ⊤) :
x + z = y + z ↔ x = y
source
theorem WithTop.add_right_cancel {α : Type u} [Add α] {x y z : WithTop α} [IsRightCancelAdd α] (hz : z ≠ ⊤) (h : x + z = y + z) :
x = y
source
theorem WithTop.add_left_inj {α : Type u} [Add α] {x y z : WithTop α} [IsLeftCancelAdd α] (hx : x ≠ ⊤) :
x + y = x + z ↔ y = z
source
theorem WithTop.add_left_cancel {α : Type u} [Add α] {x y z : WithTop α} [IsLeftCancelAdd α] (hx : x ≠ ⊤) (h : x + y = x + z) :
y = z
source
instance WithTop.addLeftMono {α : Type u} [Add α] [LE α] [AddLeftMono α] :
AddLeftMono (WithTop α)
source
instance WithTop.addRightMono {α : Type u} [Add α] [LE α] [AddRightMono α] :
AddRightMono (WithTop α)
source
instance WithTop.addLeftReflectLT {α : Type u} [Add α] [LT α] [AddLeftReflectLT α] :
AddLeftReflectLT (WithTop α)
source
instance WithTop.addRightReflectLT {α : Type u} [Add α] [LT α] [AddRightReflectLT α] :
AddRightReflectLT (WithTop α)
source
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
source
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
source
theorem WithTop.add_lt_add_left {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddLeftStrictMono α] (hx : x ≠ ⊤) :
y < z → x + y < x + z
source
theorem WithTop.add_lt_add_right {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddRightStrictMono α] (hz : z ≠ ⊤) :
x < y → x + z < y + z
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem WithTop.addLECancellable_of_ne_top {α : Type u} [Add α] {x : WithTop α} [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊤) :
AddLECancellable x
source
theorem WithTop.addLECancellable_of_lt_top {α : Type u} [Add α] {x : WithTop α} [Preorder α] [AddLeftReflectLE α] (hx : x < ⊤) :
AddLECancellable x
source
theorem WithTop.addLECancellable_coe {α : Type u} [Add α] [LE α] [AddLeftReflectLE α] (a : α) :
AddLECancellable ↑a
source
theorem WithTop.addLECancellable_iff_ne_top {α : Type u} [Add α] {x : WithTop α} [Nonempty α] [Preorder α] [AddLeftReflectLE α] :
AddLECancellable x ↔ x ≠ ⊤
source
@[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
source
instance WithTop.addSemigroup {α : Type u} [AddSemigroup α] :
AddSemigroup (WithTop α)
Equations

- WithTop.addSemigroup = { toAdd := WithTop.add, add_assoc := ⋯ }

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

- WithTop.addCommSemigroup = { toAddSemigroup := WithTop.addSemigroup, add_comm := ⋯ }

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

- WithTop.addZeroClass = { toZero := WithTop.zero, toAdd := WithTop.add, zero_add := ⋯, add_zero := ⋯ }

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

- One or more equations did not get rendered due to their size.

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 α] :
⇑addHom = some
source
instance WithTop.addCommMonoid {α : Type u} [AddCommMonoid α] :
AddCommMonoid (WithTop α)
Equations

- WithTop.addCommMonoid = { toAddMonoid := WithTop.addMonoid, add_comm := ⋯ }

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

- WithTop.addMonoidWithOne = { natCast := fun (n : ℕ) => ↑↑n, toAddMonoid := WithTop.addMonoid, toOne := WithTop.one, natCast_zero := ⋯, natCast_succ := ⋯ }

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
@[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
@[simp]
theorem WithTop.map_ofNat {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : α → β} (n : ℕ) [n.AtLeastTwo] :
map f (OfNat.ofNat n) = ↑(f (OfNat.ofNat n))
source
@[simp]
theorem WithTop.map_natCast {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : α → β} (n : ℕ) :
map f ↑n = ↑(f ↑n)
source
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
source
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
source
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
source
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
source
instance WithTop.charZero {α : Type u} [AddMonoidWithOne α] [CharZero α] :
CharZero (WithTop α)
source
instance WithTop.addCommMonoidWithOne {α : Type u} [AddCommMonoidWithOne α] :
AddCommMonoidWithOne (WithTop α)
Equations

- WithTop.addCommMonoidWithOne = { toAddMonoidWithOne := WithTop.addMonoidWithOne, add_comm := ⋯ }

source
instance WithTop.existsAddOfLE {α : Type u} [LE α] [Add α] [ExistsAddOfLE α] :
ExistsAddOfLE (WithTop α)
source
@[simp]
theorem WithTop.one_lt_top {α : Type u} [One α] [LT α] :
1 < ⊤
source
@[simp]
theorem WithTop.top_pos {α : Type u} [Zero α] [LT α] :
0 < ⊤
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 `OneHom`s.

Equations

- f.withTopMap = { toFun := WithTop.map ⇑f, map_one' := ⋯ }

Instances For

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 `ZeroHom`s

Equations

- f.withTopMap = { toFun := WithTop.map ⇑f, map_zero' := ⋯ }

Instances For

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 : M →ₙ+ N) :
WithTop M →ₙ+ WithTop N

A version of `WithTop.map` for `AddHom`s.

Equations

- f.withTopMap = { toFun := WithTop.map ⇑f, map_add' := ⋯ }

Instances For

source
@[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
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 `AddMonoidHom`s.

Equations

- f.withTopMap = { toFun := WithTop.map ⇑f, map_zero' := ⋯, 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
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 α] :
unbot 1 ⋯ = 1
source
@[simp]
theorem WithBot.unbot_zero {α : Type u} [Zero α] :
unbot 0 ⋯ = 0
source
@[simp]
theorem WithBot.unbotD_one {α : Type u} [One α] (d : α) :
unbotD d 1 = 1
source
@[simp]
theorem WithBot.unbotD_zero {α : Type u} [Zero α] (d : α) :
unbotD 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 : α → β) :
map f 1 = ↑(f 1)
source
@[simp]
theorem WithBot.map_zero {α : Type u} [Zero α] {β : Type u_1} (f : α → β) :
map f 0 = ↑(f 0)
source
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
source
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
source
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
source
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
source
instance WithBot.zeroLEOneClass {α : Type u} [One α] [Zero α] [LE α] [ZeroLEOneClass α] :
ZeroLEOneClass (WithBot α)
source
instance WithBot.add {α : Type u} [Add α] :
Add (WithBot α)
Equations

- WithBot.add = { add := Option.map₂ fun (x1 x2 : α) => x1 + x2 }

source
@[simp]
theorem WithBot.coe_add {α : Type u} [Add α] (a b : α) :
↑(a + b) = ↑a + ↑b
source
@[simp]
theorem WithBot.bot_add {α : Type u} [Add α] (x : WithBot α) :
⊥ + x = ⊥
source
@[simp]
theorem WithBot.add_bot {α : Type u} [Add α] (x : WithBot α) :
x + ⊥ = ⊥
source
@[simp]
theorem WithBot.add_eq_bot {α : Type u} [Add α] {x y : WithBot α} :
x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥
source
theorem WithBot.add_ne_bot {α : Type u} [Add α] {x y : WithBot α} :
x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥
source
@[simp]
theorem WithBot.bot_lt_add {α : Type u} [Add α] {x y : WithBot α} [LT α] :
⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y
source
theorem WithBot.add_eq_coe {α : Type u} [Add α] {a b : WithBot α} {c : α} :
a + b = ↑c ↔ ∃ (a' : α), ∃ (b' : α), ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
source
theorem WithBot.add_coe_eq_bot_iff {α : Type u} [Add α] {x : WithBot α} {b : α} :
x + ↑b = ⊥ ↔ x = ⊥
source
theorem WithBot.coe_add_eq_bot_iff {α : Type u} [Add α] {y : WithBot α} {a : α} :
↑a + y = ⊥ ↔ y = ⊥
source
theorem WithBot.add_right_inj {α : Type u} [Add α] {x y z : WithBot α} [IsRightCancelAdd α] (hz : z ≠ ⊥) :
x + z = y + z ↔ x = y
source
theorem WithBot.add_right_cancel {α : Type u} [Add α] {x y z : WithBot α} [IsRightCancelAdd α] (hz : z ≠ ⊥) (h : x + z = y + z) :
x = y
source
theorem WithBot.add_left_inj {α : Type u} [Add α] {x y z : WithBot α} [IsLeftCancelAdd α] (hx : x ≠ ⊥) :
x + y = x + z ↔ y = z
source
theorem WithBot.add_left_cancel {α : Type u} [Add α] {x y z : WithBot α} [IsLeftCancelAdd α] (hx : x ≠ ⊥) (h : x + y = x + z) :
y = z
source
instance WithBot.addLeftMono {α : Type u} [Add α] [LE α] [AddLeftMono α] :
AddLeftMono (WithBot α)
source
instance WithBot.addRightMono {α : Type u} [Add α] [LE α] [AddRightMono α] :
AddRightMono (WithBot α)
source
instance WithBot.addLeftReflectLT {α : Type u} [Add α] [LT α] [AddLeftReflectLT α] :
AddLeftReflectLT (WithBot α)
source
instance WithBot.addRightReflectLT {α : Type u} [Add α] [LT α] [AddRightReflectLT α] :
AddRightReflectLT (WithBot α)
source
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
source
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
source
theorem WithBot.add_lt_add_left {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddLeftStrictMono α] (hx : x ≠ ⊥) :
y < z → x + y < x + z
source
theorem WithBot.add_lt_add_right {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddRightStrictMono α] (hz : z ≠ ⊥) :
x < y → x + z < y + z
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem WithBot.addLECancellable_of_ne_bot {α : Type u} [Add α] {x : WithBot α} [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊥) :
AddLECancellable x
source
theorem WithBot.addLECancellable_of_lt_bot {α : Type u} [Add α] {x : WithBot α} [Preorder α] [AddLeftReflectLE α] (hx : x < ⊥) :
AddLECancellable x
source
theorem WithBot.addLECancellable_coe {α : Type u} [Add α] [LE α] [AddLeftReflectLE α] (a : α) :
AddLECancellable ↑a
source
theorem WithBot.addLECancellable_iff_ne_bot {α : Type u} [Add α] {x : WithBot α} [Nonempty α] [Preorder α] [AddLeftReflectLE α] :
AddLECancellable x ↔ x ≠ ⊥
source
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 `⊥`.

source
@[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
source
instance WithBot.AddSemigroup {α : Type u} [_root_.AddSemigroup α] :
_root_.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 α] :
⇑addHom = 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
@[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
@[simp]
theorem WithBot.map_ofNat {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : α → β} (n : ℕ) [n.AtLeastTwo] :
map f (OfNat.ofNat n) = ↑(f (OfNat.ofNat n))
source
@[simp]
theorem WithBot.map_natCast {α : Type u} {β : Type v} [AddMonoidWithOne α] {f : α → β} (n : ℕ) :
map f ↑n = ↑(f ↑n)
source
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
source
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
source
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
source
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
source
instance WithBot.charZero {α : Type u} [AddMonoidWithOne α] [CharZero α] :
CharZero (WithBot α)
source
instance WithBot.addCommMonoidWithOne {α : Type u} [AddCommMonoidWithOne α] :
AddCommMonoidWithOne (WithBot α)
Equations

- WithBot.addCommMonoidWithOne = WithTop.addCommMonoidWithOne

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 `OneHom`s.

Equations

- f.withBotMap = { toFun := WithBot.map ⇑f, map_one' := ⋯ }

Instances For

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 `ZeroHom`s

Equations

- f.withBotMap = { toFun := WithBot.map ⇑f, map_zero' := ⋯ }

Instances For

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
@[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
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 `AddHom`s.

Equations

- f.withBotMap = { toFun := WithBot.map ⇑f, map_add' := ⋯ }

Instances For

source
@[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
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 `AddMonoidHom`s.

Equations

- f.withBotMap = { toFun := WithBot.map ⇑f, map_zero' := ⋯, 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