Documentation

Mathlib.Algebra.Order.Monoid.WithTop

Adjoining top/bottom elements to ordered monoids. #

instance WithTop.zero {α : Type u} [inst : Zero α] :
Equations
  • WithTop.zero = { zero := 0 }
instance WithTop.one {α : Type u} [inst : One α] :
Equations
  • WithTop.one = { one := 1 }
@[simp]
theorem WithTop.coe_zero {α : Type u} [inst : Zero α] :
0 = 0
@[simp]
theorem WithTop.coe_one {α : Type u} [inst : One α] :
1 = 1
@[simp]
theorem WithTop.coe_eq_zero {α : Type u} [inst : Zero α] {a : α} :
a = 0 a = 0
@[simp]
theorem WithTop.coe_eq_one {α : Type u} [inst : One α] {a : α} :
a = 1 a = 1
@[simp]
theorem WithTop.untop_zero {α : Type u} [inst : Zero α] :
WithTop.untop 0 (_ : 0 ) = 0
@[simp]
theorem WithTop.untop_one {α : Type u} [inst : One α] :
WithTop.untop 1 (_ : 1 ) = 1
@[simp]
theorem WithTop.untop_zero' {α : Type u} [inst : Zero α] (d : α) :
@[simp]
theorem WithTop.untop_one' {α : Type u} [inst : One α] (d : α) :
@[simp]
theorem WithTop.coe_nonneg {α : Type u} [inst : Zero α] [inst : LE α] {a : α} :
0 a 0 a
@[simp]
theorem WithTop.one_le_coe {α : Type u} [inst : One α] [inst : LE α] {a : α} :
1 a 1 a
@[simp]
theorem WithTop.coe_le_zero {α : Type u} [inst : Zero α] [inst : LE α] {a : α} :
a 0 a 0
@[simp]
theorem WithTop.coe_le_one {α : Type u} [inst : One α] [inst : LE α] {a : α} :
a 1 a 1
@[simp]
theorem WithTop.coe_pos {α : Type u} [inst : Zero α] [inst : LT α] {a : α} :
0 < a 0 < a
@[simp]
theorem WithTop.one_lt_coe {α : Type u} [inst : One α] [inst : LT α] {a : α} :
1 < a 1 < a
@[simp]
theorem WithTop.coe_lt_zero {α : Type u} [inst : Zero α] [inst : LT α] {a : α} :
a < 0 a < 0
@[simp]
theorem WithTop.coe_lt_one {α : Type u} [inst : One α] [inst : LT α] {a : α} :
a < 1 a < 1
@[simp]
theorem WithTop.map_zero {α : Type u} [inst : Zero α] {β : Type u_1} (f : αβ) :
WithTop.map f 0 = ↑(f 0)
@[simp]
theorem WithTop.map_one {α : Type u} [inst : One α] {β : Type u_1} (f : αβ) :
WithTop.map f 1 = ↑(f 1)
@[simp]
theorem WithTop.zero_eq_coe {α : Type u} [inst : Zero α] {a : α} :
0 = a a = 0
@[simp]
theorem WithTop.one_eq_coe {α : Type u} [inst : One α] {a : α} :
1 = a a = 1
@[simp]
theorem WithTop.top_ne_zero {α : Type u} [inst : Zero α] :
abbrev WithTop.top_ne_zero.match_1 {α : Type u_1} [inst : Zero α] (motive : = 0Prop) :
(a : = 0) → motive a
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem WithTop.top_ne_one {α : Type u} [inst : One α] :
abbrev WithTop.zero_ne_top.match_1 {α : Type u_1} [inst : Zero α] (motive : 0 = Prop) :
(a : 0 = ) → motive a
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem WithTop.zero_ne_top {α : Type u} [inst : Zero α] :
@[simp]
theorem WithTop.one_ne_top {α : Type u} [inst : One α] :
instance WithTop.zeroLEOneClass {α : Type u} [inst : One α] [inst : Zero α] [inst : LE α] [inst : ZeroLEOneClass α] :
Equations
  • WithTop.zeroLEOneClass = { zero_le_one := (_ : some 0 some 1) }
instance WithTop.add {α : Type u} [inst : Add α] :
Equations
theorem WithTop.coe_add {α : Type u} [inst : Add α] {x : α} {y : α} :
↑(x + y) = x + y
theorem WithTop.coe_bit0 {α : Type u} [inst : Add α] {x : α} :
↑(bit0 x) = bit0 x
theorem WithTop.coe_bit1 {α : Type u} [inst : Add α] [inst : One α] {a : α} :
↑(bit1 a) = bit1 a
@[simp]
theorem WithTop.top_add {α : Type u} [inst : Add α] (a : WithTop α) :
@[simp]
theorem WithTop.add_top {α : Type u} [inst : Add α] (a : WithTop α) :
@[simp]
theorem WithTop.add_eq_top {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} :
a + b = a = b =
theorem WithTop.add_ne_top {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} :
theorem WithTop.add_lt_top {α : Type u} [inst : Add α] [inst : LT α] {a : WithTop α} {b : WithTop α} :
a + b < a < b <
theorem WithTop.add_eq_coe {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : α} :
a + b = c a' b', a' = a b' = b a' + b' = c
theorem WithTop.add_coe_eq_top_iff {α : Type u} [inst : Add α] {x : WithTop α} {y : α} :
x + y = x =
theorem WithTop.coe_add_eq_top_iff {α : Type u} [inst : Add α] {x : α} {y : WithTop α} :
x + y = y =
instance WithTop.covariantClass_add_le {α : Type u} [inst : Add α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] :
CovariantClass (WithTop α) (WithTop α) (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance WithTop.covariantClass_swap_add_le {α : Type u} [inst : Add α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] :
CovariantClass (WithTop α) (WithTop α) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance WithTop.contravariantClass_add_lt {α : Type u} [inst : Add α] [inst : LT α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
ContravariantClass (WithTop α) (WithTop α) (fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
instance WithTop.contravariantClass_swap_add_lt {α : Type u} [inst : Add α] [inst : LT α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
ContravariantClass (WithTop α) (WithTop α) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
theorem WithTop.le_of_add_le_add_left {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [inst : LE α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (ha : a ) (h : a + b a + c) :
b c
theorem WithTop.le_of_add_le_add_right {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [inst : LE α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (ha : a ) (h : b + a c + a) :
b c
theorem WithTop.add_lt_add_left {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ) (h : b < c) :
a + b < a + c
theorem WithTop.add_lt_add_right {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ) (h : b < c) :
b + a < c + a
theorem WithTop.add_le_add_iff_left {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (ha : a ) :
a + b a + c b c
theorem WithTop.add_le_add_iff_right {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (ha : a ) :
b + a c + a b c
theorem WithTop.add_lt_add_iff_left {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ) :
a + b < a + c b < c
theorem WithTop.add_lt_add_iff_right {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ) :
b + a < c + a b < c
theorem WithTop.add_lt_add_of_le_of_lt {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} {d : WithTop α} [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (ha : a ) (hab : a b) (hcd : c < d) :
a + c < b + d
theorem WithTop.add_lt_add_of_lt_of_le {α : Type u} [inst : Add α] {a : WithTop α} {b : WithTop α} {c : WithTop α} {d : WithTop α} [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (hc : c ) (hab : a < b) (hcd : c d) :
a + c < b + d
@[simp]
theorem WithTop.map_add {α : Type u} {β : Type v} [inst : Add α] {F : Type u_1} [inst : Add β] [inst : AddHomClass F α β] (f : F) (a : WithTop α) (b : WithTop α) :
WithTop.map (f) (a + b) = WithTop.map (f) a + WithTop.map (f) b
instance WithTop.addSemigroup {α : Type u} [inst : AddSemigroup α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
instance WithTop.addZeroClass {α : Type u} [inst : AddZeroClass α] :
Equations
  • One or more equations did not get rendered due to their size.
instance WithTop.addMonoid {α : Type u} [inst : AddMonoid α] :
Equations
  • WithTop.addMonoid = let src := WithTop.addSemigroup; let src_1 := WithTop.addZeroClass; AddMonoid.mk (_ : ∀ (a : WithTop α), 0 + a = a) (_ : ∀ (a : WithTop α), a + 0 = a) nsmulRec
instance WithTop.addCommMonoid {α : Type u} [inst : AddCommMonoid α] :
Equations
  • WithTop.addCommMonoid = let src := WithTop.addMonoid; let src_1 := WithTop.addCommSemigroup; AddCommMonoid.mk (_ : ∀ (a b : WithTop α), a + b = b + a)
Equations
  • WithTop.addMonoidWithOne = let src := WithTop.one; let src_1 := WithTop.addMonoid; AddMonoidWithOne.mk
Equations
  • WithTop.addCommMonoidWithOne = let src := WithTop.addMonoidWithOne; let src_1 := WithTop.addCommMonoid; AddCommMonoidWithOne.mk (_ : ∀ (a b : WithTop α), a + b = b + a)
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem WithTop.coe_nat {α : Type u} [inst : AddMonoidWithOne α] (n : ) :
n = n
@[simp]
theorem WithTop.nat_ne_top {α : Type u} [inst : AddMonoidWithOne α] (n : ) :
n
@[simp]
theorem WithTop.top_ne_nat {α : Type u} [inst : AddMonoidWithOne α] (n : ) :
n
def WithTop.addHom {α : Type u} [inst : AddMonoid α] :

Coercion from α to WithTop α as an AddMonoidHom.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem WithTop.zero_lt_top {α : Type u} [inst : OrderedAddCommMonoid α] :
0 <
theorem WithTop.zero_lt_coe {α : Type u} [inst : OrderedAddCommMonoid α] (a : α) :
0 < a 0 < a
def ZeroHom.withTopMap {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] (f : ZeroHom M N) :

A version of WithTop.map for ZeroHoms

Equations
def ZeroHom.withTopMap.proof_1 {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst : Zero N] (f : ZeroHom M N) :
WithTop.map (f) 0 = 0
Equations
@[simp]
theorem ZeroHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] (f : ZeroHom M N) :
@[simp]
theorem OneHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] (f : OneHom M N) :
def OneHom.withTopMap {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] (f : OneHom M N) :

A version of WithTop.map for OneHoms.

Equations
@[simp]
theorem AddHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :
def AddHom.withTopMap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :

A version of WithTop.map for AddHoms.

Equations
@[simp]
theorem AddMonoidHom.withTopMap_apply {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) :
def AddMonoidHom.withTopMap {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) :

A version of WithTop.map for AddMonoidHoms.

Equations
  • One or more equations did not get rendered due to their size.
instance WithBot.zero {α : Type u} [inst : Zero α] :
Equations
  • WithBot.zero = WithTop.zero
instance WithBot.one {α : Type u} [inst : One α] :
Equations
  • WithBot.one = WithTop.one
instance WithBot.add {α : Type u} [inst : Add α] :
Equations
  • WithBot.add = WithTop.add
instance WithBot.AddSemigroup {α : Type u} [inst : AddSemigroup α] :
Equations
  • WithBot.AddSemigroup = WithTop.addSemigroup
Equations
  • WithBot.addCommSemigroup = WithTop.addCommSemigroup
instance WithBot.addZeroClass {α : Type u} [inst : AddZeroClass α] :
Equations
  • WithBot.addZeroClass = WithTop.addZeroClass
instance WithBot.addMonoid {α : Type u} [inst : AddMonoid α] :
Equations
  • WithBot.addMonoid = WithTop.addMonoid
instance WithBot.addCommMonoid {α : Type u} [inst : AddCommMonoid α] :
Equations
  • WithBot.addCommMonoid = WithTop.addCommMonoid
Equations
  • WithBot.addMonoidWithOne = WithTop.addMonoidWithOne
Equations
  • WithBot.addCommMonoidWithOne = WithTop.addCommMonoidWithOne
instance WithBot.zeroLEOneClass {α : Type u} [inst : Zero α] [inst : One α] [inst : LE α] [inst : ZeroLEOneClass α] :
Equations
  • WithBot.zeroLEOneClass = { zero_le_one := (_ : some 0 some 1) }
theorem WithBot.coe_zero {α : Type u} [inst : Zero α] :
0 = 0
theorem WithBot.coe_one {α : Type u} [inst : One α] :
1 = 1
theorem WithBot.coe_eq_zero {α : Type u} [inst : Zero α] {a : α} :
a = 0 a = 0
theorem WithBot.coe_eq_one {α : Type u} [inst : One α] {a : α} :
a = 1 a = 1
@[simp]
theorem WithBot.unbot_zero {α : Type u} [inst : Zero α] :
WithBot.unbot 0 (_ : 0 ) = 0
@[simp]
theorem WithBot.unbot_one {α : Type u} [inst : One α] :
WithBot.unbot 1 (_ : 1 ) = 1
@[simp]
theorem WithBot.unbot_zero' {α : Type u} [inst : Zero α] (d : α) :
@[simp]
theorem WithBot.unbot_one' {α : Type u} [inst : One α] (d : α) :
@[simp]
theorem WithBot.coe_nonneg {α : Type u} [inst : Zero α] [inst : LE α] {a : α} :
0 a 0 a
@[simp]
theorem WithBot.one_le_coe {α : Type u} [inst : One α] [inst : LE α] {a : α} :
1 a 1 a
@[simp]
theorem WithBot.coe_le_zero {α : Type u} [inst : Zero α] [inst : LE α] {a : α} :
a 0 a 0
@[simp]
theorem WithBot.coe_le_one {α : Type u} [inst : One α] [inst : LE α] {a : α} :
a 1 a 1
@[simp]
theorem WithBot.coe_pos {α : Type u} [inst : Zero α] [inst : LT α] {a : α} :
0 < a 0 < a
@[simp]
theorem WithBot.one_lt_coe {α : Type u} [inst : One α] [inst : LT α] {a : α} :
1 < a 1 < a
@[simp]
theorem WithBot.coe_lt_zero {α : Type u} [inst : Zero α] [inst : LT α] {a : α} :
a < 0 a < 0
@[simp]
theorem WithBot.coe_lt_one {α : Type u} [inst : One α] [inst : LT α] {a : α} :
a < 1 a < 1
@[simp]
theorem WithBot.map_zero {α : Type u} {β : Type u_1} [inst : Zero α] (f : αβ) :
WithBot.map f 0 = ↑(f 0)
@[simp]
theorem WithBot.map_one {α : Type u} {β : Type u_1} [inst : One α] (f : αβ) :
WithBot.map f 1 = ↑(f 1)
theorem WithBot.coe_nat {α : Type u} [inst : AddMonoidWithOne α] (n : ) :
n = n
@[simp]
theorem WithBot.nat_ne_bot {α : Type u} [inst : AddMonoidWithOne α] (n : ) :
n
@[simp]
theorem WithBot.bot_ne_nat {α : Type u} [inst : AddMonoidWithOne α] (n : ) :
n
theorem WithBot.coe_add {α : Type u} [inst : Add α] (a : α) (b : α) :
↑(a + b) = a + b
theorem WithBot.coe_bit0 {α : Type u} [inst : Add α] {x : α} :
↑(bit0 x) = bit0 x
theorem WithBot.coe_bit1 {α : Type u} [inst : Add α] [inst : One α] {a : α} :
↑(bit1 a) = bit1 a
@[simp]
theorem WithBot.bot_add {α : Type u} [inst : Add α] (a : WithBot α) :
@[simp]
theorem WithBot.add_bot {α : Type u} [inst : Add α] (a : WithBot α) :
@[simp]
theorem WithBot.add_eq_bot {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} :
a + b = a = b =
theorem WithBot.add_ne_bot {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} :
theorem WithBot.bot_lt_add {α : Type u} [inst : Add α] [inst : LT α] {a : WithBot α} {b : WithBot α} :
< a + b < a < b
theorem WithBot.add_eq_coe {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {x : α} :
a + b = x a' b', a' = a b' = b a' + b' = x
theorem WithBot.add_coe_eq_bot_iff {α : Type u} [inst : Add α] {a : WithBot α} {y : α} :
a + y = a =
theorem WithBot.coe_add_eq_bot_iff {α : Type u} [inst : Add α] {b : WithBot α} {x : α} :
x + b = b =
@[simp]
theorem WithBot.map_add {α : Type u} {β : Type v} [inst : Add α] {F : Type u_1} [inst : Add β] [inst : AddHomClass F α β] (f : F) (a : WithBot α) (b : WithBot α) :
WithBot.map (f) (a + b) = WithBot.map (f) a + WithBot.map (f) b
def ZeroHom.withBotMap.proof_1 {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst : Zero N] (f : ZeroHom M N) :
WithBot.map (f) 0 = 0
Equations
def ZeroHom.withBotMap {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] (f : ZeroHom M N) :

A version of WithBot.map for ZeroHoms

Equations
@[simp]
theorem OneHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] (f : OneHom M N) :
@[simp]
theorem ZeroHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] (f : ZeroHom M N) :
def OneHom.withBotMap {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] (f : OneHom M N) :

A version of WithBot.map for OneHoms.

Equations
@[simp]
theorem AddHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :
def AddHom.withBotMap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :

A version of WithBot.map for AddHoms.

Equations
@[simp]
theorem AddMonoidHom.withBotMap_apply {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) :
def AddMonoidHom.withBotMap {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) :

A version of WithBot.map for AddMonoidHoms.

Equations
  • One or more equations did not get rendered due to their size.
instance WithBot.covariantClass_add_le {α : Type u} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] :
CovariantClass (WithBot α) (WithBot α) (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance WithBot.covariantClass_swap_add_le {α : Type u} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] :
CovariantClass (WithBot α) (WithBot α) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance WithBot.contravariantClass_add_lt {α : Type u} [inst : Add α] [inst : Preorder α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
ContravariantClass (WithBot α) (WithBot α) (fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
instance WithBot.contravariantClass_swap_add_lt {α : Type u} [inst : Add α] [inst : Preorder α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
ContravariantClass (WithBot α) (WithBot α) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
theorem WithBot.le_of_add_le_add_left {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [inst : Preorder α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (ha : a ) (h : a + b a + c) :
b c
theorem WithBot.le_of_add_le_add_right {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [inst : Preorder α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (ha : a ) (h : b + a c + a) :
b c
theorem WithBot.add_lt_add_left {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ) (h : b < c) :
a + b < a + c
theorem WithBot.add_lt_add_right {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ) (h : b < c) :
b + a < c + a
theorem WithBot.add_le_add_iff_left {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (ha : a ) :
a + b a + c b c
theorem WithBot.add_le_add_iff_right {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (ha : a ) :
b + a c + a b c
theorem WithBot.add_lt_add_iff_left {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ) :
a + b < a + c b < c
theorem WithBot.add_lt_add_iff_right {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (ha : a ) :
b + a < c + a b < c
theorem WithBot.add_lt_add_of_le_of_lt {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} {d : WithBot α} [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (hb : b ) (hab : a b) (hcd : c < d) :
a + c < b + d
theorem WithBot.add_lt_add_of_lt_of_le {α : Type u} [inst : Add α] {a : WithBot α} {b : WithBot α} {c : WithBot α} {d : WithBot α} [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (hd : d ) (hab : a < b) (hcd : c d) :
a + c < b + d
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.