Ordered Subtraction

This file proves lemmas relating (truncated) subtraction with an order. We provide a class OrderedSub 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, PartENat, ENNReal, ...)

Implementation details

OrderedSub is a mixin type-class, so that we can use the results in this file even in cases where we don't have a CanonicallyOrderedAddCommMonoid instance (even though that is our main focus). Conversely, this means we can use CanonicallyOrderedAddCommMonoid 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 [ContravariantClass α α (+) (≤)]. In the second version we replace this type-class assumption by explicit AddLECancellable 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]CommGroup with these.

TODO: generalize Nat.le_of_le_of_sub_le_sub_right, Nat.sub_le_sub_right_iff, Nat.mul_self_sub_mul_self_eq

class OrderedSub (α : Type u_3) [LE α] [Add α] [Sub α] : Prop

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

• tsub_le_iff_right : ∀ (a b c : α), a - b ≤ c ↔ a ≤ c + b

  a - b provides a lower bound on c such that a ≤ c + b.

theorem OrderedSub.tsub_le_iff_right {α : Type u_3} [LE α] [Add α] [Sub α] [self : OrderedSub α] (a : α) (b : α) (c : α) : a - b ≤ c ↔ a ≤ c + b

a - b provides a lower bound on c such that a ≤ c + b.

@[simp]

theorem tsub_le_iff_right {α : Type u_1} [LE α] [Add α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} : a - b ≤ c ↔ a ≤ c + b

theorem add_tsub_le_right {α : Type u_1} [Preorder α] [Add α] [Sub α] [OrderedSub α] {a : α} {b : α} : a + b - b ≤ a

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

theorem le_tsub_add {α : Type u_1} [Preorder α] [Add α] [Sub α] [OrderedSub α] {a : α} {b : α} : b ≤ b - a + a

Preorder

theorem tsub_le_iff_left {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} : a - b ≤ c ↔ a ≤ b + c

theorem le_add_tsub {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} : a ≤ b + (a - b)

theorem add_tsub_le_left {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} : a + b - a ≤ b

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

theorem tsub_le_tsub_right {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} (h : a ≤ b) (c : α) : a - c ≤ b - c

theorem tsub_le_iff_tsub_le {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} : a - b ≤ c ↔ a - c ≤ b

theorem tsub_tsub_le {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} : b - (b - a) ≤ a

See tsub_tsub_cancel_of_le for the equality.

theorem tsub_le_tsub_left {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : a ≤ b) (c : α) : c - b ≤ c - a

theorem tsub_le_tsub {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} {d : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c

theorem antitone_const_tsub {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {c : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : Antitone fun (x : α) => c - x

theorem add_tsub_le_assoc {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a + b - c ≤ a + (b - c)

See add_tsub_assoc_of_le for the equality.

theorem add_tsub_le_tsub_add {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a + b - c ≤ a - c + b

See tsub_add_eq_add_tsub for the equality.

theorem add_le_add_add_tsub {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a + b ≤ a + c + (b - c)

theorem le_tsub_add_add {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a + b ≤ a - c + (b + c)

theorem tsub_le_tsub_add_tsub {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a - c ≤ a - b + (b - c)

theorem tsub_tsub_tsub_le_tsub {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : c - a - (c - b) ≤ b - a

theorem tsub_tsub_le_tsub_add {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a - (b - c) ≤ a - b + c

theorem add_tsub_add_le_tsub_add_tsub {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} {d : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a + b - (c + d) ≤ a - c + (b - d)

See tsub_add_tsub_comm for the equality.

theorem add_tsub_add_le_tsub_left {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a + b - (a + c) ≤ b - c

See add_tsub_add_eq_tsub_left for the equality.

theorem add_tsub_add_le_tsub_right {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a + c - (b + c) ≤ a - b

See add_tsub_add_eq_tsub_right for the equality.

Lemmas that assume that an element is AddLECancellable

theorem AddLECancellable.le_add_tsub_swap {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} (hb : AddLECancellable b) : a ≤ b + a - b

theorem AddLECancellable.le_add_tsub {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} (hb : AddLECancellable b) : a ≤ a + b - b

theorem AddLECancellable.le_tsub_of_add_le_left {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (ha : AddLECancellable a) (h : a + b ≤ c) : b ≤ c - a

theorem AddLECancellable.le_tsub_of_add_le_right {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hb : AddLECancellable b) (h : a + b ≤ c) : a ≤ c - b

Lemmas where addition is order-reflecting

theorem le_add_tsub_swap {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a ≤ b + a - b

theorem le_add_tsub' {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a ≤ a + b - b

theorem le_tsub_of_add_le_left {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : a + b ≤ c) : b ≤ c - a

theorem le_tsub_of_add_le_right {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : a + b ≤ c) : a ≤ c - b

theorem tsub_nonpos {α : Type u_1} [Preorder α] [AddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} : a - b ≤ 0 ↔ a ≤ b

theorem tsub_nonpos_of_le {α : Type u_1} [Preorder α] [AddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} : a ≤ b → a - b ≤ 0

Alias of the reverse direction of tsub_nonpos.

Partial order

theorem tsub_tsub {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] (b : α) (a : α) (c : α) : b - a - c = b - (a + c)

theorem tsub_add_eq_tsub_tsub {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] (a : α) (b : α) (c : α) : a - (b + c) = a - b - c

theorem tsub_add_eq_tsub_tsub_swap {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] (a : α) (b : α) (c : α) : a - (b + c) = a - c - b

theorem tsub_right_comm {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} : a - b - c = a - c - b

Lemmas that assume that an element is AddLECancellable.

theorem AddLECancellable.tsub_eq_of_eq_add {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hb : AddLECancellable b) (h : a = c + b) : a - b = c

theorem AddLECancellable.eq_tsub_of_add_eq {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hc : AddLECancellable c) (h : a + c = b) : a = b - c

theorem AddLECancellable.tsub_eq_of_eq_add_rev {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hb : AddLECancellable b) (h : a = b + c) : a - b = c

@[simp]

theorem AddLECancellable.add_tsub_cancel_right {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} (hb : AddLECancellable b) : a + b - b = a

@[simp]

theorem AddLECancellable.add_tsub_cancel_left {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} (ha : AddLECancellable a) : a + b - a = b

theorem AddLECancellable.lt_add_of_tsub_lt_left {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hb : AddLECancellable b) (h : a - b < c) : a < b + c

theorem AddLECancellable.lt_add_of_tsub_lt_right {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hc : AddLECancellable c) (h : a - c < b) : a < b + c

theorem AddLECancellable.lt_tsub_of_add_lt_right {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hc : AddLECancellable c) (h : a + c < b) : a < b - c

theorem AddLECancellable.lt_tsub_of_add_lt_left {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (ha : AddLECancellable a) (h : a + c < b) : c < b - a

Lemmas where addition is order-reflecting.

theorem tsub_eq_of_eq_add {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : a = c + b) : a - b = c

theorem eq_tsub_of_add_eq {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : a + c = b) : a = b - c

theorem tsub_eq_of_eq_add_rev {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : a = b + c) : a - b = c

@[simp]

theorem add_tsub_cancel_right {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) : a + b - b = a

@[simp]

theorem add_tsub_cancel_left {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) : a + b - a = b

theorem tsub_eq_tsub_of_add_eq_add {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} {d : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : a + d = c + b) : a - b = c - d

A more general version of the reverse direction of sub_eq_sub_iff_add_eq_add

theorem lt_add_of_tsub_lt_left {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : a - b < c) : a < b + c

theorem lt_add_of_tsub_lt_right {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : a - c < b) : a < b + c

theorem lt_tsub_of_add_lt_left {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a + c < b → c < b - a

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 OrderedSub?

theorem lt_tsub_of_add_lt_right {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a + c < b → a < b - c

theorem add_tsub_add_eq_tsub_right {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (c : α) (b : α) : a + c - (b + c) = a - b

theorem add_tsub_add_eq_tsub_left {α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (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 : α} [LinearOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] (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 : α} [LinearOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] : 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 : α} [LinearOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] : 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 : α} [LinearOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] : a < b - c ↔ c < b - a

theorem lt_of_tsub_lt_tsub_left {α : Type u_1} {a : α} {b : α} {c : α} [LinearOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : a - b < a - c) : c < b

See lt_of_tsub_lt_tsub_left_of_le for a weaker statement in a partial order.

@[simp]

theorem tsub_zero {α : Type u_1} [PartialOrder α] [AddCommMonoid α] [Sub α] [OrderedSub α] (a : α) : a - 0 = a