mathlib3 documentation

algebra.order.monoid.with_top

Adjoining top/bottom elements to ordered monoids. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[protected, instance]
def with_top.has_one {α : Type u} [has_one α] :
has_one (with_top α)
Equations
source
@[protected, instance]
def with_top.has_zero {α : Type u} [has_zero α] :
has_zero (with_top α)
Equations
source
@[simp, norm_cast]
theorem with_top.coe_one {α : Type u} [has_one α] :
↑1 = 1
source
@[simp, norm_cast]
theorem with_top.coe_zero {α : Type u} [has_zero α] :
↑0 = 0
source
@[simp, norm_cast]
theorem with_top.coe_eq_zero {α : Type u} [has_zero α] {a : α} :
↑a = 0 ↔ a = 0
source
@[simp, norm_cast]
theorem with_top.coe_eq_one {α : Type u} [has_one α] {a : α} :
↑a = 1 ↔ a = 1
source
@[simp]
theorem with_top.untop_zero {α : Type u} [has_zero α] :
0.untop with_top.coe_ne_top = 0
source
@[simp]
theorem with_top.untop_one {α : Type u} [has_one α] :
1.untop with_top.coe_ne_top = 1
source
@[simp]
theorem with_top.untop_one' {α : Type u} [has_one α] (d : α) :
with_top.untop' d 1 = 1
source
@[simp]
theorem with_top.untop_zero' {α : Type u} [has_zero α] (d : α) :
with_top.untop' d 0 = 0
source
@[simp, norm_cast]
theorem with_top.one_le_coe {α : Type u} [has_one α] [has_le α] {a : α} :
1 ≤ ↑a ↔ 1 ≤ a
source
@[simp, norm_cast]
theorem with_top.coe_nonneg {α : Type u} [has_zero α] [has_le α] {a : α} :
0 ≤ ↑a ↔ 0 ≤ a
source
@[simp, norm_cast]
theorem with_top.coe_le_zero {α : Type u} [has_zero α] [has_le α] {a : α} :
↑a ≤ 0 ↔ a ≤ 0
source
@[simp, norm_cast]
theorem with_top.coe_le_one {α : Type u} [has_one α] [has_le α] {a : α} :
↑a ≤ 1 ↔ a ≤ 1
source
@[simp, norm_cast]
theorem with_top.one_lt_coe {α : Type u} [has_one α] [has_lt α] {a : α} :
1 < ↑a ↔ 1 < a
source
@[simp, norm_cast]
theorem with_top.coe_pos {α : Type u} [has_zero α] [has_lt α] {a : α} :
0 < ↑a ↔ 0 < a
source
@[simp, norm_cast]
theorem with_top.coe_lt_zero {α : Type u} [has_zero α] [has_lt α] {a : α} :
↑a < 0 ↔ a < 0
source
@[simp, norm_cast]
theorem with_top.coe_lt_one {α : Type u} [has_one α] [has_lt α] {a : α} :
↑a < 1 ↔ a < 1
source
@[protected, simp]
theorem with_top.map_zero {α : Type u} [has_zero α] {β : Type u_1} (f : α → β) :
with_top.map f 0 = ↑(f 0)
source
@[protected, simp]
theorem with_top.map_one {α : Type u} [has_one α] {β : Type u_1} (f : α → β) :
with_top.map f 1 = ↑(f 1)
source
@[simp, norm_cast]
theorem with_top.zero_eq_coe {α : Type u} [has_zero α] {a : α} :
0 = ↑a ↔ a = 0
source
@[simp, norm_cast]
theorem with_top.one_eq_coe {α : Type u} [has_one α] {a : α} :
1 = ↑a ↔ a = 1
source
@[simp]
theorem with_top.top_ne_one {α : Type u} [has_one α] :
⊤ ≠ 1
source
@[simp]
theorem with_top.top_ne_zero {α : Type u} [has_zero α] :
⊤ ≠ 0
source
@[simp]
theorem with_top.zero_ne_top {α : Type u} [has_zero α] :
0 ≠ ⊤
source
@[simp]
theorem with_top.one_ne_top {α : Type u} [has_one α] :
1 ≠ ⊤
source
@[protected, instance]
def with_top.zero_le_one_class {α : Type u} [has_one α] [has_zero α] [has_le α] [zero_le_one_class α] :
zero_le_one_class (with_top α)
Equations
source
@[protected, instance]
def with_top.has_add {α : Type u} [has_add α] :
has_add (with_top α)
Equations
source
@[norm_cast]
theorem with_top.coe_add {α : Type u} [has_add α] {x y : α} :
↑(x + y) = ↑x + ↑y
source
@[norm_cast]
theorem with_top.coe_bit0 {α : Type u} [has_add α] {x : α} :
↑(bit0 x) = bit0 ↑x
source
@[norm_cast]
theorem with_top.coe_bit1 {α : Type u} [has_add α] [has_one α] {a : α} :
↑(bit1 a) = bit1 ↑a
source
@[simp]
theorem with_top.top_add {α : Type u} [has_add α] (a : with_top α) :
⊤ + a = ⊤
source
@[simp]
theorem with_top.add_top {α : Type u} [has_add α] (a : with_top α) :
a + ⊤ = ⊤
source
@[simp]
theorem with_top.add_eq_top {α : Type u} [has_add α] {a b : with_top α} :
a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
source
theorem with_top.add_ne_top {α : Type u} [has_add α] {a b : with_top α} :
a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤
source
theorem with_top.add_lt_top {α : Type u} [has_add α] [has_lt α] {a b : with_top α} :
a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤
source
theorem with_top.add_eq_coe {α : Type u} [has_add α] {a b : with_top α} {c : α} :
a + b = ↑c ↔ ∃ (a' b' : α), ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
source
@[simp]
theorem with_top.add_coe_eq_top_iff {α : Type u} [has_add α] {x : with_top α} {y : α} :
x + ↑y = ⊤ ↔ x = ⊤
source
@[simp]
theorem with_top.coe_add_eq_top_iff {α : Type u} [has_add α] {x : α} {y : with_top α} :
↑x + y = ⊤ ↔ y = ⊤
source
@[protected, instance]
def with_top.covariant_class_add_le {α : Type u} [has_add α] [has_le α] [covariant_class α α has_add.add has_le.le] :
covariant_class (with_top α) (with_top α) has_add.add has_le.le
source
@[protected, instance]
def with_top.covariant_class_swap_add_le {α : Type u} [has_add α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] :
covariant_class (with_top α) (with_top α) (function.swap has_add.add) has_le.le
source
@[protected, instance]
def with_top.contravariant_class_add_lt {α : Type u} [has_add α] [has_lt α] [contravariant_class α α has_add.add has_lt.lt] :
contravariant_class (with_top α) (with_top α) has_add.add has_lt.lt
source
@[protected, instance]
def with_top.contravariant_class_swap_add_lt {α : Type u} [has_add α] [has_lt α] [contravariant_class α α (function.swap has_add.add) has_lt.lt] :
contravariant_class (with_top α) (with_top α) (function.swap has_add.add) has_lt.lt
source
@[protected]
theorem with_top.le_of_add_le_add_left {α : Type u} [has_add α] {a b c : with_top α} [has_le α] [contravariant_class α α has_add.add has_le.le] (ha : a ≠ ⊤) (h : a + b ≤ a + c) :
b ≤ c
source
@[protected]
theorem with_top.le_of_add_le_add_right {α : Type u} [has_add α] {a b c : with_top α} [has_le α] [contravariant_class α α (function.swap has_add.add) has_le.le] (ha : a ≠ ⊤) (h : b + a ≤ c + a) :
b ≤ c
source
@[protected]
theorem with_top.add_lt_add_left {α : Type u} [has_add α] {a b c : with_top α} [has_lt α] [covariant_class α α has_add.add has_lt.lt] (ha : a ≠ ⊤) (h : b < c) :
a + b < a + c
source
@[protected]
theorem with_top.add_lt_add_right {α : Type u} [has_add α] {a b c : with_top α} [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] (ha : a ≠ ⊤) (h : b < c) :
b + a < c + a
source
@[protected]
theorem with_top.add_le_add_iff_left {α : Type u} [has_add α] {a b c : with_top α} [has_le α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_le.le] (ha : a ≠ ⊤) :
a + b ≤ a + c ↔ b ≤ c
source
@[protected]
theorem with_top.add_le_add_iff_right {α : Type u} [has_add α] {a b c : with_top α} [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] [contravariant_class α α (function.swap has_add.add) has_le.le] (ha : a ≠ ⊤) :
b + a ≤ c + a ↔ b ≤ c
source
@[protected]
theorem with_top.add_lt_add_iff_left {α : Type u} [has_add α] {a b c : with_top α} [has_lt α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] (ha : a ≠ ⊤) :
a + b < a + c ↔ b < c
source
@[protected]
theorem with_top.add_lt_add_iff_right {α : Type u} [has_add α] {a b c : with_top α} [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] [contravariant_class α α (function.swap has_add.add) has_lt.lt] (ha : a ≠ ⊤) :
b + a < c + a ↔ b < c
source
@[protected]
theorem with_top.add_lt_add_of_le_of_lt {α : Type u} [has_add α] {a b c d : with_top α} [preorder α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a ≠ ⊤) (hab : a ≤ b) (hcd : c < d) :
a + c < b + d
source
@[protected]
theorem with_top.add_lt_add_of_lt_of_le {α : Type u} [has_add α] {a b c d : with_top α} [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hc : c ≠ ⊤) (hab : a < b) (hcd : c ≤ d) :
a + c < b + d
source
@[protected, simp]
theorem with_top.map_add {α : Type u} {β : Type v} [has_add α] {F : Type u_1} [has_add β] [add_hom_class F α β] (f : F) (a b : with_top α) :
with_top.map ⇑f (a + b) = with_top.map ⇑f a + with_top.map ⇑f b
source
@[protected, instance]
def with_top.add_semigroup {α : Type u} [add_semigroup α] :
add_semigroup (with_top α)
Equations
source
@[protected, instance]
def with_top.add_comm_semigroup {α : Type u} [add_comm_semigroup α] :
add_comm_semigroup (with_top α)
Equations
source
@[protected, instance]
def with_top.add_zero_class {α : Type u} [add_zero_class α] :
add_zero_class (with_top α)
Equations
source
@[protected, instance]
def with_top.add_monoid {α : Type u} [add_monoid α] :
add_monoid (with_top α)
Equations
source
@[protected, instance]
def with_top.add_comm_monoid {α : Type u} [add_comm_monoid α] :
add_comm_monoid (with_top α)
Equations
source
@[protected, instance]
def with_top.add_monoid_with_one {α : Type u} [add_monoid_with_one α] :
add_monoid_with_one (with_top α)
Equations
source
@[protected, instance]
def with_top.add_comm_monoid_with_one {α : Type u} [add_comm_monoid_with_one α] :
add_comm_monoid_with_one (with_top α)
Equations
source
@[protected, instance]
def with_top.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] :
ordered_add_comm_monoid (with_top α)
Equations
source
@[protected, instance]
def with_top.linear_ordered_add_comm_monoid_with_top {α : Type u} [linear_ordered_add_comm_monoid α] :
linear_ordered_add_comm_monoid_with_top (with_top α)
Equations
source
@[protected, instance]
def with_top.has_exists_add_of_le {α : Type u} [has_le α] [has_add α] [has_exists_add_of_le α] :
has_exists_add_of_le (with_top α)
source
@[protected, instance]
def with_top.canonically_ordered_add_monoid {α : Type u} [canonically_ordered_add_monoid α] :
canonically_ordered_add_monoid (with_top α)
Equations
source
@[protected, instance]
def with_top.canonically_linear_ordered_add_monoid {α : Type u} [canonically_linear_ordered_add_monoid α] :
canonically_linear_ordered_add_monoid (with_top α)
Equations
source
@[simp, norm_cast]
theorem with_top.coe_nat {α : Type u} [add_monoid_with_one α] (n : ℕ) :
↑↑n = ↑n
source
@[simp]
theorem with_top.nat_ne_top {α : Type u} [add_monoid_with_one α] (n : ℕ) :
↑n ≠ ⊤
source
@[simp]
theorem with_top.top_ne_nat {α : Type u} [add_monoid_with_one α] (n : ℕ) :
⊤ ≠ ↑n
source
def with_top.coe_add_hom {α : Type u} [add_monoid α] :
α →+ with_top α

Coercion from α to with_top α as an add_monoid_hom.

Equations
source
@[simp]
theorem with_top.coe_coe_add_hom {α : Type u} [add_monoid α] :
⇑with_top.coe_add_hom = coe
source
@[simp]
theorem with_top.zero_lt_top {α : Type u} [ordered_add_comm_monoid α] :
0 < ⊤
source
@[simp, norm_cast]
theorem with_top.zero_lt_coe {α : Type u} [ordered_add_comm_monoid α] (a : α) :
0 < ↑a ↔ 0 < a
source
@[protected]
def one_hom.with_top_map {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : one_hom M N) :
one_hom (with_top M) (with_top N)

A version of with_top.map for one_homs.

Equations
source
@[simp]
theorem zero_hom.with_top_map_apply {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : zero_hom M N) :
⇑(f.with_top_map) = with_top.map ⇑f
source
@[simp]
theorem one_hom.with_top_map_apply {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : one_hom M N) :
⇑(f.with_top_map) = with_top.map ⇑f
source
@[protected]
def zero_hom.with_top_map {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : zero_hom M N) :
zero_hom (with_top M) (with_top N)

A version of with_top.map for zero_homs

Equations
source
@[protected]
def add_hom.with_top_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :
add_hom (with_top M) (with_top N)

A version of with_top.map for add_homs.

Equations
source
@[simp]
theorem add_hom.with_top_map_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :
⇑(f.with_top_map) = with_top.map ⇑f
source
@[simp]
theorem add_monoid_hom.with_top_map_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
⇑(f.with_top_map) = with_top.map ⇑f
source
@[protected]
def add_monoid_hom.with_top_map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
with_top M →+ with_top N

A version of with_top.map for add_monoid_homs.

Equations
source
@[protected, instance]
def with_bot.has_one {α : Type u} [has_one α] :
has_one (with_bot α)
Equations
source
@[protected, instance]
def with_bot.has_zero {α : Type u} [has_zero α] :
has_zero (with_bot α)
Equations
source
@[protected, instance]
def with_bot.has_add {α : Type u} [has_add α] :
has_add (with_bot α)
Equations
source
@[protected, instance]
def with_bot.add_semigroup {α : Type u} [add_semigroup α] :
add_semigroup (with_bot α)
Equations
source
@[protected, instance]
def with_bot.add_comm_semigroup {α : Type u} [add_comm_semigroup α] :
add_comm_semigroup (with_bot α)
Equations
source
@[protected, instance]
def with_bot.add_zero_class {α : Type u} [add_zero_class α] :
add_zero_class (with_bot α)
Equations
source
@[protected, instance]
def with_bot.add_monoid {α : Type u} [add_monoid α] :
add_monoid (with_bot α)
Equations
source
@[protected, instance]
def with_bot.add_comm_monoid {α : Type u} [add_comm_monoid α] :
add_comm_monoid (with_bot α)
Equations
source
@[protected, instance]
def with_bot.add_monoid_with_one {α : Type u} [add_monoid_with_one α] :
add_monoid_with_one (with_bot α)
Equations
source
@[protected, instance]
def with_bot.add_comm_monoid_with_one {α : Type u} [add_comm_monoid_with_one α] :
add_comm_monoid_with_one (with_bot α)
Equations
source
@[protected, instance]
def with_bot.zero_le_one_class {α : Type u} [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] :
zero_le_one_class (with_bot α)
Equations
source
theorem with_bot.coe_one {α : Type u} [has_one α] :
↑1 = 1
source
theorem with_bot.coe_zero {α : Type u} [has_zero α] :
↑0 = 0
source
theorem with_bot.coe_eq_zero {α : Type u} [has_zero α] {a : α} :
↑a = 0 ↔ a = 0
source
theorem with_bot.coe_eq_one {α : Type u} [has_one α] {a : α} :
↑a = 1 ↔ a = 1
source
@[simp]
theorem with_bot.unbot_zero {α : Type u} [has_zero α] :
0.unbot with_bot.coe_ne_bot = 0
source
@[simp]
theorem with_bot.unbot_one {α : Type u} [has_one α] :
1.unbot with_bot.coe_ne_bot = 1
source
@[simp]
theorem with_bot.unbot_one' {α : Type u} [has_one α] (d : α) :
with_bot.unbot' d 1 = 1
source
@[simp]
theorem with_bot.unbot_zero' {α : Type u} [has_zero α] (d : α) :
with_bot.unbot' d 0 = 0
source
@[simp, norm_cast]
theorem with_bot.one_le_coe {α : Type u} [has_one α] [has_le α] {a : α} :
1 ≤ ↑a ↔ 1 ≤ a
source
@[simp, norm_cast]
theorem with_bot.coe_nonneg {α : Type u} [has_zero α] [has_le α] {a : α} :
0 ≤ ↑a ↔ 0 ≤ a
source
@[simp, norm_cast]
theorem with_bot.coe_le_one {α : Type u} [has_one α] [has_le α] {a : α} :
↑a ≤ 1 ↔ a ≤ 1
source
@[simp, norm_cast]
theorem with_bot.coe_le_zero {α : Type u} [has_zero α] [has_le α] {a : α} :
↑a ≤ 0 ↔ a ≤ 0
source
@[simp, norm_cast]
theorem with_bot.coe_pos {α : Type u} [has_zero α] [has_lt α] {a : α} :
0 < ↑a ↔ 0 < a
source
@[simp, norm_cast]
theorem with_bot.one_lt_coe {α : Type u} [has_one α] [has_lt α] {a : α} :
1 < ↑a ↔ 1 < a
source
@[simp, norm_cast]
theorem with_bot.coe_lt_zero {α : Type u} [has_zero α] [has_lt α] {a : α} :
↑a < 0 ↔ a < 0
source
@[simp, norm_cast]
theorem with_bot.coe_lt_one {α : Type u} [has_one α] [has_lt α] {a : α} :
↑a < 1 ↔ a < 1
source
@[protected, simp]
theorem with_bot.map_zero {α : Type u} {β : Type u_1} [has_zero α] (f : α → β) :
with_bot.map f 0 = ↑(f 0)
source
@[protected, simp]
theorem with_bot.map_one {α : Type u} {β : Type u_1} [has_one α] (f : α → β) :
with_bot.map f 1 = ↑(f 1)
source
@[norm_cast]
theorem with_bot.coe_nat {α : Type u} [add_monoid_with_one α] (n : ℕ) :
↑↑n = ↑n
source
@[simp]
theorem with_bot.nat_ne_bot {α : Type u} [add_monoid_with_one α] (n : ℕ) :
↑n ≠ ⊥
source
@[simp]
theorem with_bot.bot_ne_nat {α : Type u} [add_monoid_with_one α] (n : ℕ) :
⊥ ≠ ↑n
source
theorem with_bot.coe_add {α : Type u} [has_add α] (a b : α) :
↑(a + b) = ↑a + ↑b
source
theorem with_bot.coe_bit0 {α : Type u} [has_add α] {x : α} :
↑(bit0 x) = bit0 ↑x
source
theorem with_bot.coe_bit1 {α : Type u} [has_add α] [has_one α] {a : α} :
↑(bit1 a) = bit1 ↑a
source
@[simp]
theorem with_bot.bot_add {α : Type u} [has_add α] (a : with_bot α) :
⊥ + a = ⊥
source
@[simp]
theorem with_bot.add_bot {α : Type u} [has_add α] (a : with_bot α) :
a + ⊥ = ⊥
source
@[simp]
theorem with_bot.add_eq_bot {α : Type u} [has_add α] {a b : with_bot α} :
a + b = ⊥ ↔ a = ⊥ ∨ b = ⊥
source
theorem with_bot.add_ne_bot {α : Type u} [has_add α] {a b : with_bot α} :
a + b ≠ ⊥ ↔ a ≠ ⊥ ∧ b ≠ ⊥
source
theorem with_bot.bot_lt_add {α : Type u} [has_add α] [has_lt α] {a b : with_bot α} :
⊥ < a + b ↔ ⊥ < a ∧ ⊥ < b
source
theorem with_bot.add_eq_coe {α : Type u} [has_add α] {a b : with_bot α} {x : α} :
a + b = ↑x ↔ ∃ (a' b' : α), ↑a' = a ∧ ↑b' = b ∧ a' + b' = x
source
@[simp]
theorem with_bot.add_coe_eq_bot_iff {α : Type u} [has_add α] {a : with_bot α} {y : α} :
a + ↑y = ⊥ ↔ a = ⊥
source
@[simp]
theorem with_bot.coe_add_eq_bot_iff {α : Type u} [has_add α] {b : with_bot α} {x : α} :
↑x + b = ⊥ ↔ b = ⊥
source
@[protected, simp]
theorem with_bot.map_add {α : Type u} {β : Type v} [has_add α] {F : Type u_1} [has_add β] [add_hom_class F α β] (f : F) (a b : with_bot α) :
with_bot.map ⇑f (a + b) = with_bot.map ⇑f a + with_bot.map ⇑f b
source
@[protected]
def one_hom.with_bot_map {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : one_hom M N) :
one_hom (with_bot M) (with_bot N)

A version of with_bot.map for one_homs.

Equations
source
@[simp]
theorem zero_hom.with_bot_map_apply {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : zero_hom M N) :
⇑(f.with_bot_map) = with_bot.map ⇑f
source
@[simp]
theorem one_hom.with_bot_map_apply {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : one_hom M N) :
⇑(f.with_bot_map) = with_bot.map ⇑f
source
@[protected]
def zero_hom.with_bot_map {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : zero_hom M N) :
zero_hom (with_bot M) (with_bot N)

A version of with_bot.map for zero_homs

Equations
source
@[simp]
theorem add_hom.with_bot_map_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :
⇑(f.with_bot_map) = with_bot.map ⇑f
source
@[protected]
def add_hom.with_bot_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :
add_hom (with_bot M) (with_bot N)

A version of with_bot.map for add_homs.

Equations
source
@[protected]
def add_monoid_hom.with_bot_map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
with_bot M →+ with_bot N

A version of with_bot.map for add_monoid_homs.

Equations
source
@[simp]
theorem add_monoid_hom.with_bot_map_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
⇑(f.with_bot_map) = with_bot.map ⇑f
source
@[protected, instance]
def with_bot.covariant_class_add_le {α : Type u} [has_add α] [preorder α] [covariant_class α α has_add.add has_le.le] :
covariant_class (with_bot α) (with_bot α) has_add.add has_le.le
source
@[protected, instance]
def with_bot.covariant_class_swap_add_le {α : Type u} [has_add α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] :
covariant_class (with_bot α) (with_bot α) (function.swap has_add.add) has_le.le
source
@[protected, instance]
def with_bot.contravariant_class_add_lt {α : Type u} [has_add α] [preorder α] [contravariant_class α α has_add.add has_lt.lt] :
contravariant_class (with_bot α) (with_bot α) has_add.add has_lt.lt
source
@[protected, instance]
def with_bot.contravariant_class_swap_add_lt {α : Type u} [has_add α] [preorder α] [contravariant_class α α (function.swap has_add.add) has_lt.lt] :
contravariant_class (with_bot α) (with_bot α) (function.swap has_add.add) has_lt.lt
source
@[protected]
theorem with_bot.le_of_add_le_add_left {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [contravariant_class α α has_add.add has_le.le] (ha : a ≠ ⊥) (h : a + b ≤ a + c) :
b ≤ c
source
@[protected]
theorem with_bot.le_of_add_le_add_right {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [contravariant_class α α (function.swap has_add.add) has_le.le] (ha : a ≠ ⊥) (h : b + a ≤ c + a) :
b ≤ c
source
@[protected]
theorem with_bot.add_lt_add_left {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [covariant_class α α has_add.add has_lt.lt] (ha : a ≠ ⊥) (h : b < c) :
a + b < a + c
source
@[protected]
theorem with_bot.add_lt_add_right {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] (ha : a ≠ ⊥) (h : b < c) :
b + a < c + a
source
@[protected]
theorem with_bot.add_le_add_iff_left {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_le.le] (ha : a ≠ ⊥) :
a + b ≤ a + c ↔ b ≤ c
source
@[protected]
theorem with_bot.add_le_add_iff_right {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] [contravariant_class α α (function.swap has_add.add) has_le.le] (ha : a ≠ ⊥) :
b + a ≤ c + a ↔ b ≤ c
source
@[protected]
theorem with_bot.add_lt_add_iff_left {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] (ha : a ≠ ⊥) :
a + b < a + c ↔ b < c
source
@[protected]
theorem with_bot.add_lt_add_iff_right {α : Type u} [has_add α] {a b c : with_bot α} [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] [contravariant_class α α (function.swap has_add.add) has_lt.lt] (ha : a ≠ ⊥) :
b + a < c + a ↔ b < c
source
@[protected]
theorem with_bot.add_lt_add_of_le_of_lt {α : Type u} [has_add α] {a b c d : with_bot α} [preorder α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] (hb : b ≠ ⊥) (hab : a ≤ b) (hcd : c < d) :
a + c < b + d
source
@[protected]
theorem with_bot.add_lt_add_of_lt_of_le {α : Type u} [has_add α] {a b c d : with_bot α} [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hd : d ≠ ⊥) (hab : a < b) (hcd : c ≤ d) :
a + c < b + d
source
@[protected, instance]
def with_bot.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] :
ordered_add_comm_monoid (with_bot α)
Equations
source
@[protected, instance]
def with_bot.linear_ordered_add_comm_monoid {α : Type u} [linear_ordered_add_comm_monoid α] :
linear_ordered_add_comm_monoid (with_bot α)
Equations