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.

@[protected, instance]
def with_top.has_one {α : Type u} [has_one α] :
Equations
@[protected, instance]
def with_top.has_zero {α : Type u} [has_zero α] :
Equations
@[simp, norm_cast]
theorem with_top.coe_one {α : Type u} [has_one α] :
1 = 1
@[simp, norm_cast]
theorem with_top.coe_zero {α : Type u} [has_zero α] :
0 = 0
@[simp, norm_cast]
theorem with_top.coe_eq_zero {α : Type u} [has_zero α] {a : α} :
a = 0 a = 0
@[simp, norm_cast]
theorem with_top.coe_eq_one {α : Type u} [has_one α] {a : α} :
a = 1 a = 1
@[simp]
@[simp]
theorem with_top.untop_one {α : Type u} [has_one α] :
@[simp]
theorem with_top.untop_one' {α : Type u} [has_one α] (d : α) :
@[simp]
theorem with_top.untop_zero' {α : Type u} [has_zero α] (d : α) :
@[simp, norm_cast]
theorem with_top.one_le_coe {α : Type u} [has_one α] [has_le α] {a : α} :
1 a 1 a
@[simp, norm_cast]
theorem with_top.coe_nonneg {α : Type u} [has_zero α] [has_le α] {a : α} :
0 a 0 a
@[simp, norm_cast]
theorem with_top.coe_le_zero {α : Type u} [has_zero α] [has_le α] {a : α} :
a 0 a 0
@[simp, norm_cast]
theorem with_top.coe_le_one {α : Type u} [has_one α] [has_le α] {a : α} :
a 1 a 1
@[simp, norm_cast]
theorem with_top.one_lt_coe {α : Type u} [has_one α] [has_lt α] {a : α} :
1 < a 1 < a
@[simp, norm_cast]
theorem with_top.coe_pos {α : Type u} [has_zero α] [has_lt α] {a : α} :
0 < a 0 < a
@[simp, norm_cast]
theorem with_top.coe_lt_zero {α : Type u} [has_zero α] [has_lt α] {a : α} :
a < 0 a < 0
@[simp, norm_cast]
theorem with_top.coe_lt_one {α : Type u} [has_one α] [has_lt α] {a : α} :
a < 1 a < 1
@[protected, simp]
theorem with_top.map_zero {α : Type u} [has_zero α] {β : Type u_1} (f : α β) :
with_top.map f 0 = (f 0)
@[protected, simp]
theorem with_top.map_one {α : Type u} [has_one α] {β : Type u_1} (f : α β) :
with_top.map f 1 = (f 1)
@[simp, norm_cast]
theorem with_top.zero_eq_coe {α : Type u} [has_zero α] {a : α} :
0 = a a = 0
@[simp, norm_cast]
theorem with_top.one_eq_coe {α : Type u} [has_one α] {a : α} :
1 = a a = 1
@[simp]
theorem with_top.top_ne_one {α : Type u} [has_one α] :
@[simp]
theorem with_top.top_ne_zero {α : Type u} [has_zero α] :
@[simp]
theorem with_top.zero_ne_top {α : Type u} [has_zero α] :
@[simp]
theorem with_top.one_ne_top {α : Type u} [has_one α] :
@[protected, instance]
Equations
@[protected, instance]
def with_top.has_add {α : Type u} [has_add α] :
Equations
@[norm_cast]
theorem with_top.coe_add {α : Type u} [has_add α] {x y : α} :
(x + y) = x + y
@[norm_cast]
theorem with_top.coe_bit0 {α : Type u} [has_add α] {x : α} :
@[norm_cast]
theorem with_top.coe_bit1 {α : Type u} [has_add α] [has_one α] {a : α} :
@[simp]
theorem with_top.top_add {α : Type u} [has_add α] (a : with_top α) :
@[simp]
theorem with_top.add_top {α : Type u} [has_add α] (a : with_top α) :
@[simp]
theorem with_top.add_eq_top {α : Type u} [has_add α] {a b : with_top α} :
a + b = a = b =
theorem with_top.add_ne_top {α : Type u} [has_add α] {a b : with_top α} :
theorem with_top.add_lt_top {α : Type u} [has_add α] [has_lt α] {a b : with_top α} :
a + b < a < b <
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
@[simp]
theorem with_top.add_coe_eq_top_iff {α : Type u} [has_add α] {x : with_top α} {y : α} :
x + y = x =
@[simp]
theorem with_top.coe_add_eq_top_iff {α : Type u} [has_add α] {x : α} {y : with_top α} :
x + y = y =
@[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
@[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
@[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
@[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
@[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
@[protected]
@[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
@[protected]
@[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
@[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
@[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 α) :
@[protected, instance]
Equations
@[protected, instance]
@[simp, norm_cast]
theorem with_top.coe_nat {α : Type u} [add_monoid_with_one α] (n : ) :
@[simp]
theorem with_top.nat_ne_top {α : Type u} [add_monoid_with_one α] (n : ) :
@[simp]
theorem with_top.top_ne_nat {α : Type u} [add_monoid_with_one α] (n : ) :
def with_top.coe_add_hom {α : Type u} [add_monoid α] :

Coercion from α to with_top α as an add_monoid_hom.

Equations
@[simp]
@[simp, norm_cast]
theorem with_top.zero_lt_coe {α : Type u} [ordered_add_comm_monoid α] (a : α) :
0 < a 0 < a
@[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) :

A version of with_top.map for one_homs.

Equations
@[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) :
@[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) :
@[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) :

A version of with_top.map for zero_homs

Equations
@[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) :

A version of with_top.map for add_homs.

Equations
@[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) :
@[simp]
@[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) :

A version of with_top.map for add_monoid_homs.

Equations
@[protected, instance]
def with_bot.has_one {α : Type u} [has_one α] :
Equations
@[protected, instance]
def with_bot.has_zero {α : Type u} [has_zero α] :
Equations
@[protected, instance]
def with_bot.has_add {α : Type u} [has_add α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem with_bot.coe_one {α : Type u} [has_one α] :
1 = 1
theorem with_bot.coe_zero {α : Type u} [has_zero α] :
0 = 0
theorem with_bot.coe_eq_zero {α : Type u} [has_zero α] {a : α} :
a = 0 a = 0
theorem with_bot.coe_eq_one {α : Type u} [has_one α] {a : α} :
a = 1 a = 1
@[simp]
@[simp]
theorem with_bot.unbot_one {α : Type u} [has_one α] :
@[simp]
theorem with_bot.unbot_one' {α : Type u} [has_one α] (d : α) :
@[simp]
theorem with_bot.unbot_zero' {α : Type u} [has_zero α] (d : α) :
@[simp, norm_cast]
theorem with_bot.one_le_coe {α : Type u} [has_one α] [has_le α] {a : α} :
1 a 1 a
@[simp, norm_cast]
theorem with_bot.coe_nonneg {α : Type u} [has_zero α] [has_le α] {a : α} :
0 a 0 a
@[simp, norm_cast]
theorem with_bot.coe_le_one {α : Type u} [has_one α] [has_le α] {a : α} :
a 1 a 1
@[simp, norm_cast]
theorem with_bot.coe_le_zero {α : Type u} [has_zero α] [has_le α] {a : α} :
a 0 a 0
@[simp, norm_cast]
theorem with_bot.coe_pos {α : Type u} [has_zero α] [has_lt α] {a : α} :
0 < a 0 < a
@[simp, norm_cast]
theorem with_bot.one_lt_coe {α : Type u} [has_one α] [has_lt α] {a : α} :
1 < a 1 < a
@[simp, norm_cast]
theorem with_bot.coe_lt_zero {α : Type u} [has_zero α] [has_lt α] {a : α} :
a < 0 a < 0
@[simp, norm_cast]
theorem with_bot.coe_lt_one {α : Type u} [has_one α] [has_lt α] {a : α} :
a < 1 a < 1
@[protected, simp]
theorem with_bot.map_zero {α : Type u} {β : Type u_1} [has_zero α] (f : α β) :
with_bot.map f 0 = (f 0)
@[protected, simp]
theorem with_bot.map_one {α : Type u} {β : Type u_1} [has_one α] (f : α β) :
with_bot.map f 1 = (f 1)
@[norm_cast]
theorem with_bot.coe_nat {α : Type u} [add_monoid_with_one α] (n : ) :
@[simp]
theorem with_bot.nat_ne_bot {α : Type u} [add_monoid_with_one α] (n : ) :
@[simp]
theorem with_bot.bot_ne_nat {α : Type u} [add_monoid_with_one α] (n : ) :
theorem with_bot.coe_add {α : Type u} [has_add α] (a b : α) :
(a + b) = a + b
theorem with_bot.coe_bit0 {α : Type u} [has_add α] {x : α} :
theorem with_bot.coe_bit1 {α : Type u} [has_add α] [has_one α] {a : α} :
@[simp]
theorem with_bot.bot_add {α : Type u} [has_add α] (a : with_bot α) :
@[simp]
theorem with_bot.add_bot {α : Type u} [has_add α] (a : with_bot α) :
@[simp]
theorem with_bot.add_eq_bot {α : Type u} [has_add α] {a b : with_bot α} :
a + b = a = b =
theorem with_bot.add_ne_bot {α : Type u} [has_add α] {a b : with_bot α} :
theorem with_bot.bot_lt_add {α : Type u} [has_add α] [has_lt α] {a b : with_bot α} :
< a + b < a < b
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
@[simp]
theorem with_bot.add_coe_eq_bot_iff {α : Type u} [has_add α] {a : with_bot α} {y : α} :
a + y = a =
@[simp]
theorem with_bot.coe_add_eq_bot_iff {α : Type u} [has_add α] {b : with_bot α} {x : α} :
x + b = b =
@[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 α) :
@[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) :

A version of with_bot.map for one_homs.

Equations
@[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) :
@[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) :
@[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) :

A version of with_bot.map for zero_homs

Equations
@[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) :
@[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) :

A version of with_bot.map for add_homs.

Equations
@[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) :

A version of with_bot.map for add_monoid_homs.

Equations
@[simp]
@[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
@[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
@[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
@[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
@[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
@[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
@[protected]
@[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
@[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