Lemmas about subtraction in unbundled canonically ordered monoids

theorem add_tsub_cancel_iff_le {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} : a + (b - a) = b ↔ a ≤ b

theorem tsub_add_cancel_iff_le {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} : b - a + a = b ↔ a ≤ b

theorem tsub_eq_zero_iff_le {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} : a - b = 0 ↔ a ≤ b

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.

theorem tsub_self {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] (a : α) : a - a = 0

theorem tsub_le_self {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} : a - b ≤ a

theorem zero_tsub {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] (a : α) : 0 - a = 0

theorem tsub_self_add {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] (a : α) (b : α) : a - (a + b) = 0

theorem tsub_pos_iff_not_le {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} : 0 < a - b ↔ ¬a ≤ b

theorem tsub_pos_of_lt {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} (h : a < b) : 0 < b - a

theorem tsub_lt_of_lt {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (h : a < b) : a - c < b

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

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.

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

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

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

• CanonicallyOrderedAddCommMonoid.toAddCancelCommMonoid α = AddCancelCommMonoid.mk ⋯

Lemmas in a linearly canonically ordered monoid.

@[simp]

theorem tsub_pos_iff_lt {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} : 0 < a - b ↔ b < a

theorem tsub_eq_tsub_min {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] (a : α) (b : α) : a - b = a - min a b

theorem AddLECancellable.lt_tsub_iff_right {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hc : AddLECancellable c) : a < b - c ↔ a + c < b

theorem AddLECancellable.lt_tsub_iff_left {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hc : AddLECancellable c) : a < b - c ↔ c + a < b

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

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

theorem AddLECancellable.tsub_lt_self_iff {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} (ha : AddLECancellable a) : a - b < a ↔ 0 < a ∧ 0 < b

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.

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.

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

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

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.

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.

theorem tsub_add_eq_max {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} : a - b + b = max a b

theorem add_tsub_eq_max {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} : a + (b - a) = max a b

theorem tsub_min {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} : a - min a b = a - b

theorem tsub_add_min {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a : α} {b : α} : a - b + min a b = a

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)