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.
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]
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.
theorem
add_tsub_le_right
{α : Type u_1}
[preorder α]
[has_add α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
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 : α} :
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} :
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} :
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) :
An order isomorphism between types with ordered subtraction preserves subtraction provided that it preserves addition.
Preorder #
theorem
tsub_le_iff_left
{α : Type u_1}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
{a b c : α} :
theorem
le_add_tsub
{α : Type u_1}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
theorem
add_tsub_le_left
{α : Type u_1}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
{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 : α) :
theorem
tsub_le_iff_tsub_le
{α : Type u_1}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
{a b c : α} :
theorem
tsub_tsub_le
{α : Type u_1}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
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 : α) :
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) :
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] :
See add_tsub_assoc_of_le 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] :
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] :
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] :
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] :
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 : α} :
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) :
@[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) :
@[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) :
@[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) :
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] :
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] :
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) :
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) :
theorem
tsub_nonpos
{α : Type u_1}
[preorder α]
[add_comm_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
theorem
tsub_nonpos_of_le
{α : Type u_1}
[preorder α]
[add_comm_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
Alias of tsub_nonpos.
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 : α) :
Partial order #
theorem
tsub_tsub
{α : Type u_1}
[partial_order α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
(b a c : α) :
theorem
tsub_add_eq_tsub_tsub
{α : Type u_1}
[partial_order α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
[covariant_class α α has_add.add has_le.le]
(a b c : α) :
theorem
tsub_add_eq_tsub_tsub_swap
{α : Type u_1}
[partial_order α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
[covariant_class α α has_add.add has_le.le]
(a b c : α) :
theorem
tsub_right_comm
{α : Type u_1}
[partial_order α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[covariant_class α α has_add.add has_le.le] :
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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
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) :
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) :
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) :
@[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 : α) :
@[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 : α) :
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) :
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) :
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 : α) :
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 : α) :
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 α] :
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 α] :
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 α] :
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.
Lemmas in a canonically ordered monoid. #
@[simp]
theorem
add_tsub_cancel_of_le
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α}
(h : 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) :
theorem
add_tsub_cancel_iff_le
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
theorem
tsub_add_cancel_iff_le
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{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) :
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) :
theorem
tsub_le_tsub_iff_right
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(h : c ≤ 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) :
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.
@[simp]
theorem
tsub_eq_zero_iff_le
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
@[simp]
theorem
tsub_eq_zero_of_le
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α}
(h : a ≤ b) :
One direction of tsub_eq_zero_iff_le, as a @[simp]-lemma.
@[simp]
theorem
tsub_self
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
(a : α) :
@[simp]
theorem
tsub_le_self
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
@[simp]
theorem
tsub_zero
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
(a : α) :
@[simp]
theorem
zero_tsub
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
(a : α) :
theorem
tsub_self_add
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
(a b : α) :
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 : α} :
theorem
tsub_pos_of_lt
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α}
(h : a < b) :
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) :
theorem
tsub_tsub_tsub_cancel_right
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(h : c ≤ b) :
Lemmas that assume that an element is add_le_cancellable. #
@[protected]
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) :
@[protected]
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) :
@[protected]
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 : α) :
@[protected]
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) :
@[protected]
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) :
@[protected]
theorem
add_le_cancellable.tsub_add_tsub_comm
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c d : α}
(hb : add_le_cancellable b)
(hd : add_le_cancellable d)
(hba : b ≤ a)
(hdc : d ≤ c) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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
@[protected]
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) :
@[protected, 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) :
@[protected]
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) :
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) :
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) :
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 : α) :
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) :
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) :
theorem
tsub_add_tsub_comm
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c d : α}
[contravariant_class α α has_add.add has_le.le]
(hba : b ≤ a)
(hdc : d ≤ 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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
See tsub_tsub_le for an inequality.
Lemmas in a linearly canonically ordered monoid. #
@[simp]
theorem
tsub_pos_iff_lt
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
theorem
tsub_eq_tsub_min
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
(a b : α) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
@[protected]
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) :
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) :
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) :
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] :
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) :
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 : α} :
theorem
add_tsub_eq_max
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
theorem
tsub_min
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
theorem
tsub_add_min
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
@[protected, instance]
Equations
- with_top.has_sub = {sub := with_top.sub _inst_2}
@[protected, instance]
def
with_top.has_ordered_sub
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α] :