mathlib3 documentation

algebra.order.sub.defs

Ordered Subtraction #

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

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, part_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.

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]

structure has_ordered_sub (α : Type u_3) [has_le α] [has_add α] [has_sub α] :

Prop

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 of this typeclass

@[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

Preorder #

theorem tsub_le_iff_left {α : Type u_1} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} :

a - b ≤ c ↔ a ≤ b + c

theorem le_add_tsub {α : Type u_1} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b : α} :

a ≤ b + (a - b)

theorem add_tsub_le_left {α : Type u_1} [preorder α] [add_comm_semigroup α] [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_semigroup α] [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_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} :

a - b ≤ c ↔ a - c ≤ b

theorem tsub_tsub_le {α : Type u_1} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b : α} :

b - (b - a) ≤ a

See tsub_tsub_cancel_of_le for the equality.

theorem tsub_le_tsub_left {α : Type u_1} [preorder α] [add_comm_semigroup α] [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} [preorder α] [add_comm_semigroup α] [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 antitone_const_tsub {α : Type u_1} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {c : α} [covariant_class α α has_add.add has_le.le] :

antitone (λ (x : α), c - x)

theorem add_tsub_le_assoc {α : Type u_1} [preorder α] [add_comm_semigroup α] [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 add_tsub_le_tsub_add {α : Type u_1} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} [covariant_class α α has_add.add has_le.le] :

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 α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} [covariant_class α α has_add.add has_le.le] :

a + b ≤ a + c + (b - c)

theorem le_tsub_add_add {α : Type u_1} [preorder α] [add_comm_semigroup α] [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} [preorder α] [add_comm_semigroup α] [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} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} [covariant_class α α has_add.add has_le.le] :

c - a - (c - b) ≤ b - a

theorem tsub_tsub_le_tsub_add {α : Type u_1} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] [covariant_class α α has_add.add has_le.le] {a b c : α} :

a - (b - c) ≤ a - b + c

theorem add_tsub_add_le_tsub_add_tsub {α : Type u_1} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c d : α} [covariant_class α α has_add.add has_le.le] :

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 α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} [covariant_class α α has_add.add has_le.le] :

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 α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} [covariant_class α α has_add.add has_le.le] :

a + c - (b + c) ≤ a - b

See add_tsub_add_eq_tsub_right for the equality.

Lemmas that assume that an element is `add_le_cancellable` #

@[protected]

theorem add_le_cancellable.le_add_tsub_swap {α : Type u_1} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b : α} (hb : add_le_cancellable b) :

a ≤ b + a - b

@[protected]

theorem add_le_cancellable.le_add_tsub {α : Type u_1} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b : α} (hb : add_le_cancellable b) :

a ≤ a + b - b

@[protected]

theorem add_le_cancellable.le_tsub_of_add_le_left {α : Type u_1} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} (ha : add_le_cancellable a) (h : a + b ≤ c) :

b ≤ c - a

@[protected]

theorem add_le_cancellable.le_tsub_of_add_le_right {α : Type u_1} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} (hb : add_le_cancellable b) (h : a + b ≤ c) :

a ≤ c - b

Lemmas where addition is order-reflecting #

theorem le_add_tsub_swap {α : Type u_1} [preorder α] [add_comm_semigroup α] [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} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b : α} [contravariant_class α α has_add.add has_le.le] :

a ≤ a + b - b

theorem le_tsub_of_add_le_left {α : Type u_1} [preorder α] [add_comm_semigroup α] [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} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : a + b ≤ c) :

a ≤ c - b

theorem tsub_nonpos {α : Type u_1} [preorder α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :

a - b ≤ 0 ↔ a ≤ b

theorem tsub_nonpos_of_le {α : Type u_1} [preorder α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] {a b : α} :

a ≤ b → a - b ≤ 0

Alias of the reverse direction of tsub_nonpos.

Partial order #

theorem tsub_tsub {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] (b a c : α) :

b - a - c = b - (a + c)

theorem tsub_add_eq_tsub_tsub {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] (a b c : α) :

a - (b + c) = a - b - c

theorem tsub_add_eq_tsub_tsub_swap {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] (a b c : α) :

a - (b + c) = a - c - b

theorem tsub_right_comm {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} :

a - b - c = a - c - b

Lemmas that assume that an element is `add_le_cancellable`. #

@[protected]

theorem add_le_cancellable.tsub_eq_of_eq_add {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} (hb : add_le_cancellable b) (h : a = c + b) :

a - b = c

@[protected]

theorem add_le_cancellable.eq_tsub_of_add_eq {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} (hc : add_le_cancellable c) (h : a + c = b) :

a = b - c

@[protected]

theorem add_le_cancellable.tsub_eq_of_eq_add_rev {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} (hb : add_le_cancellable b) (h : a = b + c) :

a - b = c

@[protected, simp]

theorem add_le_cancellable.add_tsub_cancel_right {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b : α} (hb : add_le_cancellable b) :

a + b - b = a

@[protected, simp]

theorem add_le_cancellable.add_tsub_cancel_left {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b : α} (ha : add_le_cancellable a) :

a + b - a = b

@[protected]

theorem add_le_cancellable.lt_add_of_tsub_lt_left {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} (hb : add_le_cancellable b) (h : a - b < c) :

a < b + c

@[protected]

theorem add_le_cancellable.lt_add_of_tsub_lt_right {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} (hc : add_le_cancellable c) (h : a - c < b) :

a < b + c

@[protected]

theorem add_le_cancellable.lt_tsub_of_add_lt_right {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} (hc : add_le_cancellable c) (h : a + c < b) :

a < b - c

@[protected]

theorem add_le_cancellable.lt_tsub_of_add_lt_left {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} (ha : add_le_cancellable a) (h : a + c < b) :

c < b - a

Lemmas where addition is order-reflecting. #

theorem tsub_eq_of_eq_add {α : Type u_1} [partial_order α] [add_comm_semigroup α] [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_semigroup α] [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_semigroup α] [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_semigroup α] [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_semigroup α] [has_sub α] [has_ordered_sub α] [contravariant_class α α has_add.add has_le.le] (a b : α) :

a + b - a = b

theorem lt_add_of_tsub_lt_left {α : Type u_1} [partial_order α] [add_comm_semigroup α] [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_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] (h : a - c < b) :

a < b + c

theorem lt_tsub_of_add_lt_left {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] :

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

theorem lt_tsub_of_add_lt_right {α : Type u_1} [partial_order α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] {a b c : α} [contravariant_class α α has_add.add has_le.le] :

a + c < b → a < b - c

theorem add_tsub_add_eq_tsub_right {α : Type u_1} [partial_order α] [add_comm_semigroup α] [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_semigroup α] [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_semigroup α] [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_semigroup α] [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_semigroup α] [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_semigroup α] [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_semigroup α] [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.

@[simp]

theorem tsub_zero {α : Type u_1} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] (a : α) :

a - 0 = a