Documentation

Mathlib.Algebra.Order.Sub.Basic

Lemmas about subtraction in unbundled canonically ordered monoids #

source
theorem add_tsub_cancel_iff_le {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} :
a + (b - a) = b ↔ a ≤ b
source
theorem tsub_add_cancel_iff_le {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} :
b - a + a = b ↔ a ≤ b
source
theorem tsub_eq_zero_iff_le {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} :
a - b = 0 ↔ a ≤ b
source
@[simp]
theorem tsub_eq_zero_of_le {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} :
a ≤ b → a - b = 0

Alias of the reverse direction of tsub_eq_zero_iff_le.

source
theorem tsub_self {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] (a : α) :
a - a = 0
source
theorem tsub_le_self {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} :
a - b ≤ a
source
theorem zero_tsub {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] (a : α) :
0 - a = 0
source
theorem tsub_self_add {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] (a : α) (b : α) :
a - (a + b) = 0
source
theorem tsub_pos_iff_not_le {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} :
0 < a - b ↔ ¬a ≤ b
source
theorem tsub_pos_of_lt {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} (h : a < b) :
0 < b - a
source
theorem tsub_lt_of_lt {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (h : a < b) :
a - c < b
source
theorem AddLECancellable.tsub_le_tsub_iff_left {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (ha : AddLECancellable a) (hc : AddLECancellable c) (h : c ≤ a) :
a - b ≤ a - c ↔ c ≤ b
source
theorem AddLECancellable.tsub_right_inj {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (ha : AddLECancellable a) (hb : AddLECancellable b) (hc : AddLECancellable c) (hba : b ≤ a) (hca : c ≤ a) :
a - b = a - c ↔ b = c

Lemmas where addition is order-reflecting. #

source
theorem tsub_le_tsub_iff_left {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : c ≤ a) :
a - b ≤ a - c ↔ c ≤ b
source
theorem tsub_right_inj {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (hba : b ≤ a) (hca : c ≤ a) :
a - b = a - c ↔ b = c
source
@[reducible, inline]
abbrev CanonicallyOrderedAddCommMonoid.toAddCancelCommMonoid (α : Type u_1) [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] :
AddCancelCommMonoid α

A CanonicallyOrderedAddCommMonoid with ordered subtraction and order-reflecting addition is cancellative. This is not an instance as it would form a typeclass loop.

See note [reducible non-instances].

Equations
Instances For

    Lemmas in a linearly canonically ordered monoid. #

    source
    @[simp]
    theorem tsub_pos_iff_lt {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} :
    0 < a - b ↔ b < a
    source
    theorem tsub_eq_tsub_min {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] (a : α) (b : α) :
    a - b = a - min a b
    source
    theorem AddLECancellable.lt_tsub_iff_right {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hc : AddLECancellable c) :
    a < b - c ↔ a + c < b
    source
    theorem AddLECancellable.lt_tsub_iff_left {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hc : AddLECancellable c) :
    a < b - c ↔ c + a < b
    source
    theorem AddLECancellable.tsub_lt_tsub_iff_right {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hc : AddLECancellable c) (h : c ≤ a) :
    a - c < b - c ↔ a < b
    source
    theorem AddLECancellable.tsub_lt_self {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} (ha : AddLECancellable a) (h₁ : 0 < a) (h₂ : 0 < b) :
    a - b < a
    source
    theorem AddLECancellable.tsub_lt_self_iff {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} (ha : AddLECancellable a) :
    a - b < a ↔ 0 < a ∧ 0 < b
    source
    theorem AddLECancellable.tsub_lt_tsub_iff_left_of_le {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (ha : AddLECancellable a) (hb : AddLECancellable 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.

    source
    theorem tsub_lt_tsub_iff_right {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : c ≤ a) :
    a - c < b - c ↔ a < b

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

    source
    theorem tsub_lt_self {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] :
    0 < a → 0 < b → a - b < a
    source
    @[simp]
    theorem tsub_lt_self_iff {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] :
    a - b < a ↔ 0 < a ∧ 0 < b
    source
    theorem tsub_lt_tsub_iff_left_of_le {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (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.

    source
    theorem tsub_tsub_eq_min {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) :
    a - (a - b) = min a b

    Lemmas about max and min. #

    source
    theorem tsub_add_eq_max {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} :
    a - b + b = max a b
    source
    theorem add_tsub_eq_max {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} :
    a + (b - a) = max a b
    source
    theorem tsub_min {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} :
    a - min a b = a - b
    source
    theorem tsub_add_min {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} :
    a - b + min a b = a
    source
    theorem Even.tsub {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {m : α} {n : α} (hm : Even m) (hn : Even n) :
    Even (m - n)