mathlib documentation

algebra.order.sub

Ordered Subtraction #

This file proves lemmas relating (truncated) subtraction with an order. We provide a class has_ordered_sub stating that a - b ≤ c ↔ a ≤ c + b.

The subtraction discussed here could both be normal subtraction in an additive group or truncated subtraction on a canonically ordered monoid (, multiset, enat, ennreal, ...)

Implementation details #

has_ordered_sub is a mixin type-class, so that we can use the results in this file even in cases where we don't have a canonically_ordered_add_monoid instance (even though that is our main focus). Conversely, this means we can use canonically_ordered_add_monoid without necessarily having to define a subtraction.

The results in this file are ordered by the type-class assumption needed to prove it. This means that similar results might not be close to each other. Furthermore, we don't prove implications if a bi-implication can be proven under the same assumptions.

Lemmas using this class are named using tsub instead of sub (short for "truncated subtraction"). This is to avoid naming conflicts with similar lemmas about ordered groups.

We provide a second version of most results that require [contravariant_class α α (+) (≤)]. In the second version we replace this type-class assumption by explicit add_le_cancellable assumptions.

TODO: maybe we should make a multiplicative version of this, so that we can replace some identical lemmas about subtraction/division in ordered_[add_]comm_group with these.

@[class]
structure has_ordered_sub (α : Type u_3) [has_le α] [has_add α] [has_sub α] :
Type
  • tsub_le_iff_right : ∀ (a b c : α), a - b c a c + b

has_ordered_sub α means that α has a subtraction characterized by a - b ≤ c ↔ a ≤ c + b. In other words, a - b is the least c such that a ≤ b + c.

This is satisfied both by the subtraction in additive ordered groups and by truncated subtraction in canonically ordered monoids on many specific types.

Instances
@[simp]
theorem tsub_le_iff_right {α : Type u_1} [preorder α] [has_add α] [has_sub α] [has_ordered_sub α] {a b c : α} :
a - b c a c + b
theorem add_tsub_le_right {α : Type u_1} [preorder α] [has_add α] [has_sub α] [has_ordered_sub α] {a b : α} :
a + b - b a

See add_tsub_cancel_right for the equality if contravariant_class α α (+) (≤).

theorem le_tsub_add {α : Type u_1} [preorder α] [has_add α] [has_sub α] [has_ordered_sub α] {a b : α} :
b b - a + a
theorem add_hom.le_map_tsub {α : Type u_1} {β : Type u_2} [preorder α] [has_add α] [has_sub α] [has_ordered_sub α] [preorder β] [has_add β] [has_sub β] [has_ordered_sub β] (f : add_hom α β) (hf : monotone f) (a b : α) :
f a - f b f (a - b)
theorem le_mul_tsub {R : Type u_1} [distrib R] [preorder R] [has_sub R] [has_ordered_sub R] [covariant_class R R has_mul.mul has_le.le] {a b c : R} :
a * b - a * c a * (b - c)
theorem le_tsub_mul {R : Type u_1} [comm_semiring R] [preorder R] [has_sub R] [has_ordered_sub R] [covariant_class R R has_mul.mul has_le.le] {a b c : R} :
a * c - b * c (a - b) * c
theorem order_iso.map_tsub {M : Type u_1} {N : Type u_2} [preorder M] [has_add M] [has_sub M] [has_ordered_sub M] [partial_order N] [has_add N] [has_sub N] [has_ordered_sub N] (e : M ≃o N) (h_add : ∀ (a b : M), e (a + b) = e a + e b) (a b : M) :
e (a - b) = e a - e b

An order isomorphism between types with ordered subtraction preserves subtraction provided that it preserves addition.

theorem tsub_le_iff_left {α : Type u_1} [preorder α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} :
a - b c a b + c
theorem le_add_tsub {α : Type u_1} [preorder α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :
a b + (a - b)
theorem add_tsub_le_left {α : Type u_1} [preorder α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :
a + b - a b

See add_tsub_cancel_left for the equality if contravariant_class α α (+) (≤).

theorem tsub_le_tsub_right {α : Type u_1} [preorder α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} (h : a b) (c : α) :
a - c b - c
theorem tsub_le_iff_tsub_le {α : Type u_1} [preorder α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} :
a - b c a - c b
theorem tsub_tsub_le {α : Type u_1} [preorder α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :
b - (b - a) a

See tsub_tsub_cancel_of_le for the equality.

theorem add_monoid_hom.le_map_tsub {α : Type u_1} {β : Type u_2} [preorder α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] [preorder β] [add_comm_monoid β] [has_sub β] [has_ordered_sub β] (f : α →+ β) (hf : monotone f) (a b : α) :
f a - f b f (a - b)
theorem tsub_tsub {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] (b a c : α) :
b - a - c = b - (a + c)
theorem tsub_le_tsub_left {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} [covariant_class α α has_add.add has_le.le] (h : a b) (c : α) :
c - b c - a
theorem tsub_le_tsub {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c d : α} [covariant_class α α has_add.add has_le.le] (hab : a b) (hcd : c d) :
a - d b - c
theorem tsub_add_eq_tsub_tsub {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [covariant_class α α has_add.add has_le.le] :
a - (b + c) = a - b - c
theorem tsub_add_eq_tsub_tsub_swap {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [covariant_class α α has_add.add has_le.le] :
a - (b + c) = a - c - b
theorem add_le_add_add_tsub {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [covariant_class α α has_add.add has_le.le] :
a + b a + c + (b - c)
theorem tsub_right_comm {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [covariant_class α α has_add.add has_le.le] :
a - b - c = a - c - b
theorem add_tsub_le_assoc {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [covariant_class α α has_add.add has_le.le] :
a + b - c a + (b - c)

See add_tsub_assoc_of_le for the equality.

theorem le_tsub_add_add {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [covariant_class α α has_add.add has_le.le] :
a + b a - c + (b + c)
theorem tsub_le_tsub_add_tsub {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [covariant_class α α has_add.add has_le.le] :
a - c a - b + (b - c)
theorem tsub_tsub_tsub_le_tsub {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [covariant_class α α has_add.add has_le.le] :
c - a - (c - b) b - a

Lemmas that assume that an element is add_le_cancellable. #

theorem add_le_cancellable.le_add_tsub_swap {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} (hb : add_le_cancellable b) :
a b + a - b
theorem add_le_cancellable.le_add_tsub {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} (hb : add_le_cancellable b) :
a a + b - b
theorem add_le_cancellable.tsub_eq_of_eq_add {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hb : add_le_cancellable b) (h : a = c + b) :
a - b = c
theorem add_le_cancellable.eq_tsub_of_add_eq {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hc : add_le_cancellable c) (h : a + c = b) :
a = b - c
theorem add_le_cancellable.tsub_eq_of_eq_add_rev {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hb : add_le_cancellable b) (h : a = b + c) :
a - b = c
@[simp]
theorem add_le_cancellable.add_tsub_cancel_right {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} (hb : add_le_cancellable b) :
a + b - b = a
@[simp]
theorem add_le_cancellable.add_tsub_cancel_left {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} (ha : add_le_cancellable a) :
a + b - a = b
theorem add_le_cancellable.le_tsub_of_add_le_left {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (ha : add_le_cancellable a) (h : a + b c) :
b c - a
theorem add_le_cancellable.le_tsub_of_add_le_right {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hb : add_le_cancellable b) (h : a + b c) :
a c - b
theorem add_le_cancellable.lt_add_of_tsub_lt_left {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hb : add_le_cancellable b) (h : a - b < c) :
a < b + c
theorem add_le_cancellable.lt_add_of_tsub_lt_right {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hc : add_le_cancellable c) (h : a - c < b) :
a < b + c

Lemmas where addition is order-reflecting. #

theorem le_add_tsub_swap {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} [contravariant_class α α has_add.add has_le.le] :
a b + a - b
theorem le_add_tsub' {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} [contravariant_class α α has_add.add has_le.le] :
a a + b - b
theorem tsub_eq_of_eq_add {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : a = c + b) :
a - b = c
theorem eq_tsub_of_add_eq {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : a + c = b) :
a = b - c
theorem tsub_eq_of_eq_add_rev {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : a = b + c) :
a - b = c
@[simp]
theorem add_tsub_cancel_right {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] [contravariant_class α α has_add.add has_le.le] (a b : α) :
a + b - b = a
@[simp]
theorem add_tsub_cancel_left {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] [contravariant_class α α has_add.add has_le.le] (a b : α) :
a + b - a = b
theorem le_tsub_of_add_le_left {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : a + b c) :
b c - a
theorem le_tsub_of_add_le_right {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : a + b c) :
a c - b
theorem lt_add_of_tsub_lt_left {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : a - b < c) :
a < b + c
theorem lt_add_of_tsub_lt_right {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : a - c < b) :
a < b + c
theorem add_tsub_add_right_eq_tsub {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_le.le] (a c b : α) :
a + c - (b + c) = a - b
theorem add_tsub_add_eq_tsub_left {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_le.le] (a b c : α) :
a + b - (a + c) = b - c

Lemmas in a linearly ordered monoid. #

theorem lt_of_tsub_lt_tsub_right {α : Type u_1} {a b c : α} [linear_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] (h : a - c < b - c) :
a < b

See lt_of_tsub_lt_tsub_right_of_le for a weaker statement in a partial order.

theorem lt_tsub_iff_right {α : Type u_1} {a b c : α} [linear_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] :
a < b - c a + c < b

See lt_tsub_iff_right_of_le for a weaker statement in a partial order.

theorem lt_tsub_iff_left {α : Type u_1} {a b c : α} [linear_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] :
a < b - c c + a < b

See lt_tsub_iff_left_of_le for a weaker statement in a partial order.

theorem lt_tsub_comm {α : Type u_1} {a b c : α} [linear_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] :
a < b - c c < b - a
theorem lt_of_tsub_lt_tsub_left {α : Type u_1} {a b c : α} [linear_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] [covariant_class α α has_add.add has_le.le] (h : a - b < a - c) :
c < b

See lt_of_tsub_lt_tsub_left_of_le for a weaker statement in a partial order.

Lemmas in a canonically ordered monoid. #

theorem add_tsub_cancel_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} (h : a b) :
a + (b - a) = b
theorem tsub_add_cancel_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} (h : a b) :
b - a + a = b
theorem add_tsub_cancel_iff_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :
a + (b - a) = b a b
theorem tsub_add_cancel_iff_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :
b - a + a = b a b
theorem add_le_of_le_tsub_right_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (h : b c) (h2 : a c - b) :
a + b c
theorem add_le_of_le_tsub_left_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (h : a c) (h2 : b c - a) :
a + b c
theorem tsub_le_tsub_iff_right {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (h : c b) :
a - c b - c a b
theorem tsub_left_inj {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (h1 : c a) (h2 : c b) :
a - c = b - c a = b
theorem lt_of_tsub_lt_tsub_right_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (h : c b) (h2 : a - c < b - c) :
a < b

See lt_of_tsub_lt_tsub_right for a stronger statement in a linear order.

theorem tsub_eq_zero_iff_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :
a - b = 0 a b
@[simp]
theorem tsub_self {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] (a : α) :
a - a = 0
@[simp]
theorem tsub_le_self {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :
a - b a
@[simp]
theorem tsub_zero {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] (a : α) :
a - 0 = a
@[simp]
theorem zero_tsub {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] (a : α) :
0 - a = 0
theorem tsub_self_add {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] (a b : α) :
a - (a + b) = 0
theorem tsub_inj_left {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (h₁ : a b) (h₂ : a c) (h₃ : b - a = c - a) :
b = c
theorem tsub_pos_iff_not_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :
0 < a - b ¬a b
theorem tsub_pos_of_lt {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} (h : a < b) :
0 < b - a
theorem tsub_add_tsub_cancel {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hab : b a) (hbc : c b) :
a - b + (b - c) = a - c
theorem tsub_tsub_tsub_cancel_right {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (h : c b) :
a - c - (b - c) = a - b

Lemmas that assume that an element is add_le_cancellable. #

theorem add_le_cancellable.eq_tsub_iff_add_eq_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hc : add_le_cancellable c) (h : c b) :
a = b - c a + c = b
theorem add_le_cancellable.tsub_eq_iff_eq_add_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hb : add_le_cancellable b) (h : b a) :
a - b = c a = c + b
theorem add_le_cancellable.add_tsub_assoc_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {b c : α} (hc : add_le_cancellable c) (h : c b) (a : α) :
a + b - c = a + (b - c)
theorem add_le_cancellable.tsub_add_eq_add_tsub {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hb : add_le_cancellable b) (h : b a) :
a - b + c = a + c - b
theorem add_le_cancellable.tsub_tsub_assoc {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hbc : add_le_cancellable (b - c)) (h₁ : b a) (h₂ : c b) :
a - (b - c) = a - b + c
theorem add_le_cancellable.le_tsub_iff_left {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (ha : add_le_cancellable a) (h : a c) :
b c - a a + b c
theorem add_le_cancellable.le_tsub_iff_right {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (ha : add_le_cancellable a) (h : a c) :
b c - a b + a c
theorem add_le_cancellable.tsub_lt_iff_left {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hb : add_le_cancellable b) (hba : b a) :
a - b < c a < b + c
theorem add_le_cancellable.tsub_lt_iff_right {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hb : add_le_cancellable b) (hba : b a) :
a - b < c a < c + b
theorem add_le_cancellable.lt_tsub_of_add_lt_right {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hc : add_le_cancellable c) (h : a + c < b) :
a < b - c
theorem add_le_cancellable.lt_tsub_of_add_lt_left {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (ha : add_le_cancellable a) (h : a + c < b) :
c < b - a
theorem add_le_cancellable.tsub_lt_iff_tsub_lt {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hb : add_le_cancellable b) (hc : add_le_cancellable c) (h₁ : b a) (h₂ : c a) :
a - b < c a - c < b
theorem add_le_cancellable.le_tsub_iff_le_tsub {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (ha : add_le_cancellable a) (hc : add_le_cancellable c) (h₁ : a b) (h₂ : c b) :
a b - c c b - a
theorem add_le_cancellable.lt_tsub_iff_right_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hc : add_le_cancellable c) (h : c b) :
a < b - c a + c < b
theorem add_le_cancellable.lt_tsub_iff_left_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hc : add_le_cancellable c) (h : c b) :
a < b - c c + a < b
theorem add_le_cancellable.lt_of_tsub_lt_tsub_left_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_lt.lt] (hb : add_le_cancellable b) (hca : c a) (h : a - b < a - c) :
c < b
theorem add_le_cancellable.tsub_le_tsub_iff_left {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (ha : add_le_cancellable a) (hc : add_le_cancellable c) (h : c a) :
a - b a - c c b
theorem add_le_cancellable.tsub_right_inj {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (ha : add_le_cancellable a) (hb : add_le_cancellable b) (hc : add_le_cancellable c) (hba : b a) (hca : c a) :
a - b = a - c b = c
theorem add_le_cancellable.tsub_lt_tsub_right_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hc : add_le_cancellable c) (h : c a) (h2 : a < b) :
a - c < b - c
theorem add_le_cancellable.tsub_inj_right {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hab : add_le_cancellable (a - b)) (h₁ : b a) (h₂ : c a) (h₃ : a - b = a - c) :
b = c
theorem add_le_cancellable.tsub_lt_tsub_iff_left_of_le_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_lt.lt] (hb : add_le_cancellable b) (hab : add_le_cancellable (a - b)) (h₁ : b a) (h₂ : c a) :
a - b < a - c c < b
@[simp]
theorem add_le_cancellable.add_tsub_tsub_cancel {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hac : add_le_cancellable (a - c)) (h : c a) :
a + b - (a - c) = b + c
theorem add_le_cancellable.tsub_tsub_cancel_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} (hba : add_le_cancellable (b - a)) (h : a b) :
b - (b - a) = a

Lemmas where addition is order-reflecting. #

theorem eq_tsub_iff_add_eq_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : c b) :
a = b - c a + c = b
theorem tsub_eq_iff_eq_add_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : b a) :
a - b = c a = c + b
theorem add_tsub_assoc_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {b c : α} [contravariant_class α α has_add.add has_le.le] (h : c b) (a : α) :
a + b - c = a + (b - c)

See add_tsub_le_assoc for an inequality.

theorem tsub_add_eq_add_tsub {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : b a) :
a - b + c = a + c - b
theorem tsub_tsub_assoc {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h₁ : b a) (h₂ : c b) :
a - (b - c) = a - b + c
theorem le_tsub_iff_left {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : a c) :
b c - a a + b c
theorem le_tsub_iff_right {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : a c) :
b c - a b + a c
theorem tsub_lt_iff_left {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (hbc : b a) :
a - b < c a < b + c
theorem tsub_lt_iff_right {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (hbc : b a) :
a - b < c a < c + b
theorem lt_tsub_of_add_lt_right {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : a + c < b) :
a < b - c

This lemma (and some of its corollaries also holds for ennreal, but this proof doesn't work for it. Maybe we should add this lemma as field to has_ordered_sub?

theorem lt_tsub_of_add_lt_left {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : a + c < b) :
c < b - a
theorem tsub_lt_iff_tsub_lt {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h₁ : b a) (h₂ : c a) :
a - b < c a - c < b
theorem le_tsub_iff_le_tsub {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h₁ : a b) (h₂ : c b) :
a b - c c b - a
theorem lt_tsub_iff_right_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : c b) :
a < b - c a + c < b

See lt_tsub_iff_right for a stronger statement in a linear order.

theorem lt_tsub_iff_left_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : c b) :
a < b - c c + a < b

See lt_tsub_iff_left for a stronger statement in a linear order.

theorem lt_of_tsub_lt_tsub_left_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] (hca : c a) (h : a - b < a - c) :
c < b

See lt_of_tsub_lt_tsub_left for a stronger statement in a linear order.

theorem tsub_le_tsub_iff_left {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : c a) :
a - b a - c c b
theorem tsub_right_inj {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (hba : b a) (hca : c a) :
a - b = a - c b = c
theorem tsub_lt_tsub_right_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : c a) (h2 : a < b) :
a - c < b - c
theorem tsub_inj_right {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h₁ : b a) (h₂ : c a) (h₃ : a - b = a - c) :
b = c
theorem tsub_lt_tsub_iff_left_of_le_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] (h₁ : b a) (h₂ : c a) :
a - b < a - c c < b

See tsub_lt_tsub_iff_left_of_le for a stronger statement in a linear order.

@[simp]
theorem add_tsub_tsub_cancel {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : c a) :
a + b - (a - c) = b + c
theorem tsub_tsub_cancel_of_le {α : Type u_1} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} [contravariant_class α α has_add.add has_le.le] (h : a b) :
b - (b - a) = a

See tsub_tsub_le for an inequality.

Lemmas in a linearly canonically ordered monoid. #

theorem tsub_pos_iff_lt {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :
0 < a - b b < a
theorem tsub_eq_tsub_min {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] (a b : α) :
a - b = a - min a b
theorem add_le_cancellable.lt_tsub_iff_right {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hc : add_le_cancellable c) :
a < b - c a + c < b
theorem add_le_cancellable.lt_tsub_iff_left {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hc : add_le_cancellable c) :
a < b - c c + a < b
theorem add_le_cancellable.tsub_lt_tsub_iff_right {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (hc : add_le_cancellable c) (h : c a) :
a - c < b - c a < b
theorem add_le_cancellable.tsub_lt_self {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} (ha : add_le_cancellable a) (hb : add_le_cancellable b) (h₁ : 0 < a) (h₂ : 0 < b) :
a - b < a
theorem add_le_cancellable.tsub_lt_self_iff {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} (ha : add_le_cancellable a) (hb : add_le_cancellable b) :
a - b < a 0 < a 0 < b
theorem add_le_cancellable.tsub_lt_tsub_iff_left_of_le {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} (ha : add_le_cancellable a) (hb : add_le_cancellable b) (h : b a) :
a - b < a - c c < b

See lt_tsub_iff_left_of_le_of_le for a weaker statement in a partial order.

theorem tsub_lt_tsub_iff_right {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : c a) :
a - c < b - c a < b

This lemma also holds for ennreal, but we need a different proof for that.

theorem tsub_lt_self {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} [contravariant_class α α has_add.add has_le.le] (h₁ : 0 < a) (h₂ : 0 < b) :
a - b < a
theorem tsub_lt_self_iff {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} [contravariant_class α α has_add.add has_le.le] :
a - b < a 0 < a 0 < b
theorem tsub_lt_tsub_iff_left_of_le {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : b a) :
a - b < a - c c < b

See lt_tsub_iff_left_of_le_of_le for a weaker statement in a partial order.

Lemmas about max and min. #

theorem tsub_add_eq_max {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :
a - b + b = max a b
theorem add_tsub_eq_max {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :
a + (b - a) = max a b
theorem tsub_min {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :
a - min a b = a - b
theorem tsub_add_min {α : Type u_1} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :
a - b + min a b = a
def with_top.sub {α : Type u_1} [has_sub α] [has_zero α] (a b : with_top α) :

If α has subtraction and 0, we can extend the subtraction to with_top α.

Equations
@[instance]
def with_top.has_sub {α : Type u_1} [has_sub α] [has_zero α] :
Equations
@[simp]
theorem with_top.coe_sub {α : Type u_1} [has_sub α] [has_zero α] {a b : α} :
(a - b) = a - b
@[simp]
theorem with_top.top_sub_coe {α : Type u_1} [has_sub α] [has_zero α] {a : α} :
@[simp]
theorem with_top.sub_top {α : Type u_1} [has_sub α] [has_zero α] {a : with_top α} :
a - = 0