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 α] :

untop 1 ⋯ = 1

source

@[simp]

theorem WithTop.untop_zero {α : Type u} [Zero α] :

untop 0 ⋯ = 0

source

@[simp]

theorem WithTop.untop_one' {α : Type u} [One α] (d : α) :

untop' d 1 = 1

source

@[simp]

theorem WithTop.untop_zero' {α : Type u} [Zero α] (d : α) :

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 : α → β) :

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 α] (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 b : WithTop α} :

a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

source

theorem WithTop.add_ne_top {α : Type u} [Add α] {a b : WithTop α} :

a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤

source

theorem WithTop.add_lt_top {α : Type u} [Add α] [LT α] {a b : WithTop α} :

a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

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 α} {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 b c : WithTop α} [IsRightCancelAdd α] (ha : a ≠ ⊤) :

b + a = c + a ↔ b = c

source

theorem WithTop.add_right_cancel {α : Type u} [Add α] {a b c : WithTop α} [IsRightCancelAdd α] (ha : a ≠ ⊤) (h : b + a = c + a) :

b = c

source

theorem WithTop.add_left_cancel_iff {α : Type u} [Add α] {a b c : WithTop α} [IsLeftCancelAdd α] (ha : a ≠ ⊤) :

a + b = a + c ↔ b = c

source

theorem WithTop.add_left_cancel {α : Type u} [Add α] {a b c : WithTop α} [IsLeftCancelAdd α] (ha : a ≠ ⊤) (h : a + b = a + c) :

b = c

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 α] {a b 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 b c : WithTop α} [LE α] [AddRightReflectLE α] (ha : a ≠ ⊤) (h : b + a ≤ c + a) :

b ≤ c

source

theorem WithTop.add_lt_add_left {α : Type u} [Add α] {a b c : WithTop α} [LT α] [AddLeftStrictMono α] (ha : a ≠ ⊤) (h : b < c) :

a + b < a + c

source

theorem WithTop.add_lt_add_right {α : Type u} [Add α] {a b 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 b 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 b 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 b 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 b 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 b c 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 b c d : WithTop α} [Preorder α] [AddLeftMono α] [AddRightStrictMono α] (hc : c ≠ ⊤) (hab : a < b) (hcd : c ≤ d) :

a + c < b + d

source

theorem WithTop.addLECancellable_of_ne_top {α : Type u} [Add α] {a : WithTop α} [Preorder α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (ha : a ≠ ⊤) :

AddLECancellable a

source

theorem WithTop.addLECancellable_of_lt_top {α : Type u} [Add α] {a : WithTop α} [Preorder α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (ha : a < ⊤) :

AddLECancellable a

source

theorem WithTop.addLECancellable_coe {α : Type u} [Add α] [Preorder α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) :

AddLECancellable ↑a

source

theorem WithTop.addLECancellable_iff_ne_top {α : Type u} [Add α] {a : WithTop α} [Nonempty α] [Preorder α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] :

AddLECancellable a ↔ a ≠ ⊤

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 = AddSemigroup.mk ⋯

source

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

AddCommSemigroup (WithTop α)

Equations

WithTop.addCommSemigroup = AddCommSemigroup.mk ⋯

source

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

AddZeroClass (WithTop α)

Equations

WithTop.addZeroClass = AddZeroClass.mk ⋯ ⋯

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 α] :

⇑addHom = some

source

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

AddCommMonoid (WithTop α)

Equations

WithTop.addCommMonoid = AddCommMonoid.mk ⋯

source

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

AddMonoidWithOne (WithTop α)

Equations

WithTop.addMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯

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 = AddCommMonoidWithOne.mk ⋯

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

@[deprecated WithTop.top_pos (since := "2024-10-22")]

theorem WithTop.zero_lt_top {α : Type u} [Zero α] [LT α] :

0 < ⊤

Alias of WithTop.top_pos.

source

@[deprecated WithTop.coe_pos (since := "2024-10-22")]

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' := ⋯ }

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 ZeroHoms

Equations

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

Instances For

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

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

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.

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 AddMonoidHoms.

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.unbot_one' {α : Type u} [One α] (d : α) :

unbot' d 1 = 1

source

@[simp]

theorem WithBot.unbot_zero' {α : Type u} [Zero α] (d : α) :

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 : α → β) :

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 = WithTop.add

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

@[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 b : WithBot α} :

a + b = ⊥ ↔ a = ⊥ ∨ b = ⊥

source

theorem WithBot.add_ne_bot {α : Type u} [Add α] {a b : WithBot α} :

a + b ≠ ⊥ ↔ a ≠ ⊥ ∧ b ≠ ⊥

source

theorem WithBot.bot_lt_add {α : Type u} [Add α] [LT α] {a b : WithBot α} :

⊥ < a + b ↔ ⊥ < a ∧ ⊥ < b

source

theorem WithBot.add_eq_coe {α : Type u} [Add α] {a 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 b c : WithBot α} [IsRightCancelAdd α] (ha : a ≠ ⊥) :

b + a = c + a ↔ b = c

source

theorem WithBot.add_right_cancel {α : Type u} [Add α] {a b c : WithBot α} [IsRightCancelAdd α] (ha : a ≠ ⊥) (h : b + a = c + a) :

b = c

source

theorem WithBot.add_left_cancel_iff {α : Type u} [Add α] {a b c : WithBot α} [IsLeftCancelAdd α] (ha : a ≠ ⊥) :

a + b = a + c ↔ b = c

source

theorem WithBot.add_left_cancel {α : Type u} [Add α] {a b 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 b : WithBot α) :

map (⇑f) (a + b) = map (⇑f) a + 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' := ⋯ }

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 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 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.

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 AddMonoidHoms.

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

source

instance WithBot.addLeftMono {α : Type u} [Add α] [Preorder α] [AddLeftMono α] :

AddLeftMono (WithBot α)

source

instance WithBot.addRightMono {α : Type u} [Add α] [Preorder α] [AddRightMono α] :

AddRightMono (WithBot α)

source

instance WithBot.addLeftReflectLT {α : Type u} [Add α] [Preorder α] [AddLeftReflectLT α] :

AddLeftReflectLT (WithBot α)

source

instance WithBot.addRightReflectLT {α : Type u} [Add α] [Preorder α] [AddRightReflectLT α] :

AddRightReflectLT (WithBot α)

source

theorem WithBot.le_of_add_le_add_left {α : Type u} [Add α] {a b 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 b c : WithBot α} [Preorder α] [AddRightReflectLE α] (ha : a ≠ ⊥) (h : b + a ≤ c + a) :

b ≤ c

source

theorem WithBot.add_lt_add_left {α : Type u} [Add α] {a b c : WithBot α} [Preorder α] [AddLeftStrictMono α] (ha : a ≠ ⊥) (h : b < c) :

a + b < a + c

source

theorem WithBot.add_lt_add_right {α : Type u} [Add α] {a b 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 b 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 b 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 b 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 b 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 b c 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 b c d : WithBot α} [Preorder α] [AddLeftMono α] [AddRightStrictMono α] (hd : d ≠ ⊥) (hab : a < b) (hcd : c ≤ d) :

a + c < b + d

Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Adjoining top/bottom elements to ordered monoids. #