Loogle!

Result

Found 260 declarations mentioning OrderedSub. Of these, only the first 200 are shown.

OrderedSub 📋 Mathlib.Algebra.Order.Sub.Defs
(α : Type u_2) [LE α] [Add α] [Sub α] : Prop
add_tsub_le_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [Add α] [Sub α] [OrderedSub α] {a b : α} : a + b - b ≤ a
le_tsub_add 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [Add α] [Sub α] [OrderedSub α] {a b : α} : b ≤ b - a + a
tsub_le_iff_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [LE α] [Add α] [Sub α] [OrderedSub α] {a b c : α} : a - b ≤ c ↔ a ≤ c + b
OrderedSub.mk 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_2} [LE α] [Add α] [Sub α] (tsub_le_iff_right : ∀ (a b c : α), a - b ≤ c ↔ a ≤ c + b) : OrderedSub α
OrderedSub.tsub_le_iff_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_2} {inst✝ : LE α} {inst✝¹ : Add α} {inst✝² : Sub α} [self : OrderedSub α] (a b c : α) : a - b ≤ c ↔ a ≤ c + b
tsub_tsub_le 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} : b - (b - a) ≤ a
antitone_const_tsub 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {c : α} [AddLeftMono α] : Antitone fun x => c - x
add_tsub_le_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} : a + b - a ≤ b
le_add_tsub 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} : a ≤ b + (a - b)
tsub_zero 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommMonoid α] [Sub α] [OrderedSub α] (a : α) : a - 0 = a
tsub_le_tsub_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} (h : a ≤ b) (c : α) : a - c ≤ b - c
tsub_le_iff_tsub_le 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} : a - b ≤ c ↔ a - c ≤ b
tsub_le_iff_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} : a - b ≤ c ↔ a ≤ b + c
le_add_tsub' 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} [AddLeftReflectLE α] : a ≤ a + b - b
le_add_tsub_swap 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} [AddLeftReflectLE α] : a ≤ b + a - b
tsub_nonpos_of_le 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommMonoid α] [Sub α] [OrderedSub α] {a b : α} : a ≤ b → a - b ≤ 0
add_tsub_cancel_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] (a b : α) : a + b - a = b
add_tsub_cancel_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] (a b : α) : a + b - b = a
tsub_nonpos 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommMonoid α] [Sub α] [OrderedSub α] {a b : α} : a - b ≤ 0 ↔ a ≤ b
AddLECancellable.le_add_tsub 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} (hb : AddLECancellable b) : a ≤ a + b - b
AddLECancellable.le_add_tsub_swap 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} (hb : AddLECancellable b) : a ≤ b + a - b
tsub_right_comm 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} : a - b - c = a - c - b
AddLECancellable.add_tsub_cancel_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} (ha : AddLECancellable a) : a + b - a = b
AddLECancellable.add_tsub_cancel_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} (hb : AddLECancellable b) : a + b - b = a
tsub_le_tsub_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} [AddLeftMono α] (h : a ≤ b) (c : α) : c - b ≤ c - a
eq_tsub_of_add_eq 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a + c = b) : a = b - c
tsub_add_eq_tsub_tsub 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] (a b c : α) : a - (b + c) = a - b - c
tsub_add_eq_tsub_tsub_swap 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] (a b c : α) : a - (b + c) = a - c - b
tsub_eq_of_eq_add 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a = c + b) : a - b = c
tsub_eq_of_eq_add_rev 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a = b + c) : a - b = c
tsub_tsub 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] (b a c : α) : b - a - c = b - (a + c)
AddLECancellable.eq_tsub_of_add_eq 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} (hc : AddLECancellable c) (h : a + c = b) : a = b - c
AddLECancellable.tsub_eq_of_eq_add 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} (hb : AddLECancellable b) (h : a = c + b) : a - b = c
AddLECancellable.tsub_eq_of_eq_add_rev 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} (hb : AddLECancellable b) (h : a = b + c) : a - b = c
le_tsub_of_add_le_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a + b ≤ c) : b ≤ c - a
le_tsub_of_add_le_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a + b ≤ c) : a ≤ c - b
AddLECancellable.le_tsub_of_add_le_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} (ha : AddLECancellable a) (h : a + b ≤ c) : b ≤ c - a
AddLECancellable.le_tsub_of_add_le_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} (hb : AddLECancellable b) (h : a + b ≤ c) : a ≤ c - b
tsub_le_tsub 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c d : α} [AddLeftMono α] (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c
tsub_tsub_tsub_le_tsub 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftMono α] : c - a - (c - b) ≤ b - a
lt_add_of_tsub_lt_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a - b < c) : a < b + c
lt_add_of_tsub_lt_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a - c < b) : a < b + c
lt_tsub_of_add_lt_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] : a + c < b → c < b - a
lt_tsub_of_add_lt_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] : a + c < b → a < b - c
tsub_le_tsub_add_tsub 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftMono α] : a - c ≤ a - b + (b - c)
tsub_tsub_le_tsub_add 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] {a b c : α} : a - (b - c) ≤ a - b + c
AddLECancellable.lt_add_of_tsub_lt_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} (hb : AddLECancellable b) (h : a - b < c) : a < b + c
AddLECancellable.lt_add_of_tsub_lt_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} (hc : AddLECancellable c) (h : a - c < b) : a < b + c
AddLECancellable.lt_tsub_of_add_lt_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} (ha : AddLECancellable a) (h : a + c < b) : c < b - a
AddLECancellable.lt_tsub_of_add_lt_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} (hc : AddLECancellable c) (h : a + c < b) : a < b - c
AddLECancellable.eq_tsub_of_add_eq' 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftMono α] (hb : AddLECancellable b) (h : a + c = b) : a = b - c
AddLECancellable.tsub_eq_of_eq_add' 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftMono α] (ha : AddLECancellable a) (h : a = c + b) : a - b = c
AddLECancellable.tsub_eq_of_eq_add_rev' 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftMono α] (ha : AddLECancellable a) (h : a = b + c) : a - b = c
add_tsub_add_le_tsub_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftMono α] : a + b - (a + c) ≤ b - c
add_tsub_add_le_tsub_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftMono α] : a + c - (b + c) ≤ a - b
add_tsub_le_assoc 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftMono α] : a + b - c ≤ a + (b - c)
add_tsub_le_tsub_add 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftMono α] : a + b - c ≤ a - c + b
lt_of_tsub_lt_tsub_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} {a b c : α} [LinearOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] (h : a - c < b - c) : a < b
add_le_add_add_tsub 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftMono α] : a + b ≤ a + c + (b - c)
le_tsub_add_add 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftMono α] : a + b ≤ a - c + (b + c)
lt_tsub_comm 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} {a b c : α} [LinearOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] : a < b - c ↔ c < b - a
tsub_eq_tsub_of_add_eq_add 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c d : α} [AddLeftReflectLE α] (h : a + d = c + b) : a - b = c - d
lt_tsub_iff_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} {a b c : α} [LinearOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] : a < b - c ↔ c + a < b
lt_tsub_iff_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} {a b c : α} [LinearOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] : a < b - c ↔ a + c < b
add_tsub_add_eq_tsub_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] [AddLeftReflectLE α] (a b c : α) : a + b - (a + c) = b - c
add_tsub_add_eq_tsub_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] [AddLeftReflectLE α] (a c b : α) : a + c - (b + c) = a - b
add_tsub_add_le_tsub_add_tsub 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c d : α} [AddLeftMono α] : a + b - (c + d) ≤ a - c + (b - d)
lt_of_tsub_lt_tsub_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} {a b c : α} [LinearOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] (h : a - b < a - c) : c < b
AddGroup.toOrderedSub 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u_1} [AddGroup α] [LE α] [AddRightMono α] : OrderedSub α
Nat.instOrderedSub 📋 Mathlib.Algebra.Order.Group.Nat
: OrderedSub ℕ
add_tsub_cancel_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b : α} (h : a ≤ b) : a + (b - a) = b
tsub_add_cancel_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b : α} (h : a ≤ b) : b - a + a = b
tsub_tsub_cancel_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b : α} [AddLeftReflectLE α] (h : a ≤ b) : b - (b - a) = a
tsub_inj_left 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (h₁ : a ≤ b) (h₂ : a ≤ c) : b - a = c - a → b = c
lt_of_tsub_lt_tsub_right_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (h : c ≤ b) (h2 : a - c < b - c) : a < b
tsub_left_inj 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (h1 : c ≤ a) (h2 : c ≤ b) : a - c = b - c ↔ a = b
tsub_le_tsub_iff_right 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (h : c ≤ b) : a - c ≤ b - c ↔ a ≤ b
tsub_tsub_tsub_cancel_right 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (h : c ≤ b) : a - c - (b - c) = a - b
add_le_of_le_tsub_left_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (h : a ≤ c) (h2 : b ≤ c - a) : a + b ≤ c
add_le_of_le_tsub_right_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (h : b ≤ c) (h2 : a ≤ c - b) : a + b ≤ c
AddLECancellable.tsub_tsub_cancel_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b : α} (hba : AddLECancellable (b - a)) (h : a ≤ b) : b - (b - a) = a
eq_tsub_iff_add_eq_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ b) : a = b - c ↔ a + c = b
tsub_eq_iff_eq_add_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : b ≤ a) : a - b = c ↔ a = c + b
AddLECancellable.eq_tsub_iff_add_eq_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hc : AddLECancellable c) (h : c ≤ b) : a = b - c ↔ a + c = b
AddLECancellable.tsub_eq_iff_eq_add_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hb : AddLECancellable b) (h : b ≤ a) : a - b = c ↔ a = c + b
tsub_inj_right 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h₁ : b ≤ a) (h₂ : c ≤ a) (h₃ : a - b = a - c) : b = c
tsub_lt_tsub_left_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] : b ≤ a → c < b → a - b < a - c
tsub_lt_tsub_right_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ a) (h2 : a < b) : a - c < b - c
AddLECancellable.tsub_lt_tsub_right_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hc : AddLECancellable c) (h : c ≤ a) (h2 : a < b) : a - c < b - c
tsub_tsub_tsub_cancel_left 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : b ≤ a) : a - c - (a - b) = b - c
tsub_add_tsub_cancel 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hab : b ≤ a) (hcb : c ≤ b) : a - b + (b - c) = a - c
le_tsub_iff_left 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a ≤ c) : b ≤ c - a ↔ a + b ≤ c
le_tsub_iff_right 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a ≤ c) : b ≤ c - a ↔ b + a ≤ c
lt_tsub_iff_left_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ b) : a < b - c ↔ c + a < b
lt_tsub_iff_right_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ b) : a < b - c ↔ a + c < b
tsub_lt_iff_left 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (hbc : b ≤ a) : a - b < c ↔ a < b + c
tsub_lt_iff_right 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (hbc : b ≤ a) : a - b < c ↔ a < c + b
tsub_tsub_eq_add_tsub_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ b) : a - (b - c) = a + c - b
AddLECancellable.le_tsub_iff_left 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (ha : AddLECancellable a) (h : a ≤ c) : b ≤ c - a ↔ a + b ≤ c
AddLECancellable.le_tsub_iff_right 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (ha : AddLECancellable a) (h : a ≤ c) : b ≤ c - a ↔ b + a ≤ c
AddLECancellable.lt_tsub_iff_left_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hc : AddLECancellable c) (h : c ≤ b) : a < b - c ↔ c + a < b
AddLECancellable.lt_tsub_iff_right_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hc : AddLECancellable c) (h : c ≤ b) : a < b - c ↔ a + c < b
AddLECancellable.tsub_lt_iff_left 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hb : AddLECancellable b) (hba : b ≤ a) : a - b < c ↔ a < b + c
AddLECancellable.tsub_lt_iff_right 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hb : AddLECancellable b) (hba : b ≤ a) : a - b < c ↔ a < c + b
AddLECancellable.tsub_inj_right 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a) (h₃ : a - b = a - c) : b = c
AddLECancellable.tsub_lt_tsub_left_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h : c < b) : a - b < a - c
add_tsub_assoc_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {b c : α} [AddLeftReflectLE α] (h : c ≤ b) (a : α) : a + b - c = a + (b - c)
add_tsub_tsub_cancel 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ a) : a + b - (a - c) = b + c
le_tsub_iff_le_tsub 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h₁ : a ≤ b) (h₂ : c ≤ b) : a ≤ b - c ↔ c ≤ b - a
tsub_add_eq_add_tsub 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : b ≤ a) : a - b + c = a + c - b
tsub_lt_iff_tsub_lt 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < c ↔ a - c < b
AddLECancellable.add_tsub_assoc_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {b c : α} (hc : AddLECancellable c) (h : c ≤ b) (a : α) : a + b - c = a + (b - c)
AddLECancellable.tsub_add_eq_add_tsub 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hb : AddLECancellable b) (h : b ≤ a) : a - b + c = a + c - b
AddLECancellable.tsub_tsub_tsub_cancel_left 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hab : AddLECancellable (a - b)) (h : b ≤ a) : a - c - (a - b) = b - c
lt_of_tsub_lt_tsub_left_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] [AddLeftReflectLT α] (hca : c ≤ a) (h : a - b < a - c) : c < b
AddLECancellable.lt_of_tsub_lt_tsub_left_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLT α] (hb : AddLECancellable b) (hca : c ≤ a) (h : a - b < a - c) : c < b
add_add_tsub_cancel 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (hcb : c ≤ b) : a + c + (b - c) = a + b
tsub_tsub_assoc 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h₁ : b ≤ a) (h₂ : c ≤ b) : a - (b - c) = a - b + c
AddLECancellable.add_add_tsub_cancel 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hc : AddLECancellable c) (hcb : c ≤ b) : a + c + (b - c) = a + b
AddLECancellable.add_tsub_tsub_cancel 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hac : AddLECancellable (a - c)) (h : c ≤ a) : a + b - (a - c) = b + c
tsub_lt_tsub_iff_left_of_le_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] [AddLeftReflectLT α] (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < a - c ↔ c < b
AddLECancellable.le_tsub_iff_le_tsub 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (ha : AddLECancellable a) (hc : AddLECancellable c) (h₁ : a ≤ b) (h₂ : c ≤ b) : a ≤ b - c ↔ c ≤ b - a
AddLECancellable.tsub_lt_iff_tsub_lt 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hb : AddLECancellable b) (hc : AddLECancellable c) (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < c ↔ a - c < b
AddLECancellable.tsub_tsub_assoc 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hbc : AddLECancellable (b - c)) (h₁ : b ≤ a) (h₂ : c ≤ b) : a - (b - c) = a - b + c
tsub_add_tsub_comm 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c d : α} [AddLeftReflectLE α] (hba : b ≤ a) (hdc : d ≤ c) : a - b + (c - d) = a + c - (b + d)
AddLECancellable.tsub_lt_tsub_iff_left_of_le_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLT α] (hb : AddLECancellable b) (hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < a - c ↔ c < b
AddLECancellable.tsub_add_tsub_comm 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c d : α} (hb : AddLECancellable b) (hd : AddLECancellable d) (hba : b ≤ a) (hdc : d ≤ c) : a - b + (c - d) = a + c - (b + d)
CanonicallyOrderedAddCommMonoid.toAddCancelCommMonoid 📋 Mathlib.Algebra.Order.Sub.Basic
(α : Type u_1) [AddCommMonoid α] [PartialOrder α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] : AddCancelCommMonoid α
tsub_le_self 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} : a - b ≤ a
tsub_self 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] (a : α) : a - a = 0
tsub_lt_of_lt 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b c : α} (h : a < b) : a - c < b
tsub_eq_zero_of_le 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} : a ≤ b → a - b = 0
tsub_eq_zero_iff_le 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} : a - b = 0 ↔ a ≤ b
add_tsub_cancel_iff_le 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} : a + (b - a) = b ↔ a ≤ b
tsub_add_cancel_iff_le 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} : b - a + a = b ↔ a ≤ b
zero_tsub 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] (a : α) : 0 - a = 0
CanonicallyOrderedAdd.toOrderedSub 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [AddRightReflectLE α] : OrderedSub α
tsub_pos_of_lt 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} (h : a < b) : 0 < b - a
tsub_self_add 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] (a b : α) : a - (a + b) = 0
tsub_pos_iff_not_le 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} : 0 < a - b ↔ ¬a ≤ b
tsub_eq_tsub_min 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] (a b : α) : a - b = a - min a b
tsub_min 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} : a - min a b = a - b
add_tsub_eq_max 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} : a + (b - a) = max a b
tsub_add_eq_max 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} : a - b + b = max a b
tsub_add_min 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} : a - b + min a b = a
tsub_right_inj 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c
tsub_le_tsub_iff_left 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ a) : a - b ≤ a - c ↔ c ≤ b
tsub_tsub_eq_min 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] (a b : α) : a - (a - b) = min a b
tsub_pos_iff_lt 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} : 0 < a - b ↔ b < a
AddLECancellable.lt_tsub_iff_left 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [Sub α] [OrderedSub α] {a b c : α} (hc : AddLECancellable c) : a < b - c ↔ c + a < b
AddLECancellable.lt_tsub_iff_right 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [Sub α] [OrderedSub α] {a b c : α} (hc : AddLECancellable c) : a < b - c ↔ a + c < b
AddLECancellable.tsub_le_tsub_iff_left 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b c : α} (ha : AddLECancellable a) (hc : AddLECancellable c) (h : c ≤ a) : a - b ≤ a - c ↔ c ≤ b
Even.tsub 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] {m n : α} (hm : Even m) (hn : Even n) : Even (m - n)
AddLECancellable.tsub_right_inj 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [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
tsub_lt_tsub_iff_left_of_le 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : b ≤ a) : a - b < a - c ↔ c < b
tsub_lt_tsub_iff_right 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ a) : a - c < b - c ↔ a < b
AddLECancellable.tsub_lt_tsub_iff_right 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b c : α} (hc : AddLECancellable c) (h : c ≤ a) : a - c < b - c ↔ a < b
tsub_lt_self 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} [AddLeftReflectLE α] : 0 < a → 0 < b → a - b < a
AddLECancellable.tsub_lt_self 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} (ha : AddLECancellable a) (h₁ : 0 < a) (h₂ : 0 < b) : a - b < a
tsub_lt_self_iff 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} [AddLeftReflectLE α] : a - b < a ↔ 0 < a ∧ 0 < b
AddLECancellable.tsub_lt_self_iff 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} (ha : AddLECancellable a) : a - b < a ↔ 0 < a ∧ 0 < b
AddLECancellable.tsub_lt_tsub_iff_left_of_le 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b c : α} (ha : AddLECancellable a) (hb : AddLECancellable b) (h : b ≤ a) : a - b < a - c ↔ c < b
Nat.cast_tsub 📋 Mathlib.Data.Nat.Cast.Order.Ring
{α : Type u_2} [CommSemiring α] [PartialOrder α] [IsOrderedRing α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] (m n : ℕ) : ↑(m - n) = ↑m - ↑n
Nat.ceil_sub_natCast 📋 Mathlib.Algebra.Order.Floor.Semiring
{R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) : ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n
Nat.floor_sub_natCast 📋 Mathlib.Algebra.Order.Floor.Semiring
{R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) : ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
Nat.ceil_sub_one 📋 Mathlib.Algebra.Order.Floor.Semiring
{R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) : ⌈a - 1⌉₊ = ⌈a⌉₊ - 1
Nat.floor_sub_one 📋 Mathlib.Algebra.Order.Floor.Semiring
{R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) : ⌊a - 1⌋₊ = ⌊a⌋₊ - 1
Nat.ceil_sub_ofNat 📋 Mathlib.Algebra.Order.Floor.Semiring
{R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) [n.AtLeastTwo] : ⌈a - OfNat.ofNat n⌉₊ = ⌈a⌉₊ - OfNat.ofNat n
Nat.floor_sub_ofNat 📋 Mathlib.Algebra.Order.Floor.Semiring
{R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) [n.AtLeastTwo] : ⌊a - OfNat.ofNat n⌋₊ = ⌊a⌋₊ - OfNat.ofNat n
mul_tsub 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [NonUnitalNonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] (a b c : R) : a * (b - c) = a * b - a * c
mul_tsub_one 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [NonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] (a b : R) : a * (b - 1) = a * b - a
tsub_mul 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [NonUnitalNonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] [MulRightMono R] (a b c : R) : (a - b) * c = a * c - b * c
AddLECancellable.mul_tsub 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [NonUnitalNonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] {a b c : R} (h : AddLECancellable (a * c)) : a * (b - c) = a * b - a * c
tsub_one_mul 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [NonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [MulRightMono R] [AddLeftReflectLE R] (a b : R) : (a - 1) * b = a * b - b
mul_self_tsub_mul_self 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] (a b : R) : a * a - b * b = (a + b) * (a - b)
AddLECancellable.tsub_mul 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [NonUnitalNonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [MulRightMono R] {a b c : R} (h : AddLECancellable (b * c)) : (a - b) * c = a * c - b * c
sq_tsub_sq 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] (a b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b)
mul_self_tsub_one 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] (a : R) : a * a - 1 = (a + 1) * (a - 1)
tsub_div 📋 Mathlib.Algebra.Order.Field.Canonical
{α : Type u_1} [Semifield α] [LinearOrder α] [CanonicallyOrderedAdd α] [IsStrictOrderedRing α] [Sub α] [OrderedSub α] (a b c : α) : (a - b) / c = a / c - b / c
Nonneg.orderedSub 📋 Mathlib.Algebra.Order.Nonneg.Ring
{α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] : OrderedSub (Nonneg α)
Multiset.instOrderedSub 📋 Mathlib.Algebra.Order.Group.Multiset
{α : Type u_1} [DecidableEq α] : OrderedSub (Multiset α)
Multiset.sum_map_tsub 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
{ι : Type u_2} {M : Type u_5} [AddCommMonoid M] [PartialOrder M] [ExistsAddOfLE M] [AddLeftMono M] [AddLeftReflectLE M] [Sub M] [OrderedSub M] (l : Multiset ι) {f g : ι → M} (hfg : ∀ x ∈ l, g x ≤ f x) : (Multiset.map (fun x => f x - g x) l).sum = (Multiset.map f l).sum - (Multiset.map g l).sum
Finset.sum_range_tsub 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] [PartialOrder M] [Sub M] [OrderedSub M] [AddLeftMono M] [AddLeftReflectLE M] [ExistsAddOfLE M] {f : ℕ → M} (h : Monotone f) (n : ℕ) : ∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0
Finset.sum_tsub_distrib 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [Sub M] [OrderedSub M] [AddLeftMono M] [AddLeftReflectLE M] [ExistsAddOfLE M] (s : Finset ι) {f g : ι → M} (hfg : ∀ x ∈ s, g x ≤ f x) : ∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x
WithTop.instOrderedSub 📋 Mathlib.Algebra.Order.Sub.WithTop
{α : Type u_1} [Add α] [LE α] [OrderBot α] [Sub α] [OrderedSub α] : OrderedSub (WithTop α)
instOrderedSubENat 📋 Mathlib.Data.ENat.Monoid
: OrderedSub ℕ∞
Finset.prod_Ico_add_right_sub_eq 📋 Mathlib.Algebra.BigOperators.Intervals
{α : Type u_1} {M : Type u_3} [CommMonoid M] {f : α → M} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [Sub α] [OrderedSub α] (a b c : α) : ∏ x ∈ Finset.Ico (a + c) (b + c), f (x - c) = ∏ x ∈ Finset.Ico a b, f x
Finset.sum_Ico_add_right_sub_eq 📋 Mathlib.Algebra.BigOperators.Intervals
{α : Type u_1} {M : Type u_3} [AddCommMonoid M] {f : α → M} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [Sub α] [OrderedSub α] (a b c : α) : ∑ x ∈ Finset.Ico (a + c) (b + c), f (x - c) = ∑ x ∈ Finset.Ico a b, f x
Finset.HasAntidiagonal.filter_fst_eq_antidiagonal 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Sub A] [OrderedSub A] [AddLeftReflectLE A] [Finset.HasAntidiagonal A] (n m : A) [DecidablePred fun x => x = m] [Decidable (m ≤ n)] : {x ∈ Finset.HasAntidiagonal.antidiagonal n | x.1 = m} = if m ≤ n then {(m, n - m)} else ∅
Finset.HasAntidiagonal.filter_snd_eq_antidiagonal 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Sub A] [OrderedSub A] [AddLeftReflectLE A] [Finset.HasAntidiagonal A] (n m : A) [DecidablePred fun x => x = m] [Decidable (m ≤ n)] : {x ∈ Finset.HasAntidiagonal.antidiagonal n | x.2 = m} = if m ≤ n then {(n - m, m)} else ∅
Finset.add_sup'' 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} (hs : s.Nonempty) (f : ι → M) (a : M) : a + s.sup' hs f = s.sup' hs fun i => a + f i
Finset.sup'_add' 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] (s : Finset ι) (f : ι → M) (a : M) (hs : s.Nonempty) : s.sup' hs f + a = s.sup' hs fun i => f i + a
Finset.add_sup 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} [OrderBot M] (hs : s.Nonempty) (f : ι → M) (a : M) : a + s.sup f = s.sup fun i => a + f i
Finset.sup_add 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} [OrderBot M] (hs : s.Nonempty) (f : ι → M) (a : M) : s.sup f + a = s.sup fun i => f i + a
Finset.sup_add_sup 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} {t : Finset κ} [OrderBot M] (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → M) (g : κ → M) : s.sup f + t.sup g = (s ×ˢ t).sup fun ij => f ij.1 + g ij.2
Finsupp.tsub 📋 Mathlib.Data.Finsupp.Order
{ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] : Sub (ι →₀ α)
Finsupp.orderedSub 📋 Mathlib.Data.Finsupp.Order
{ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] : OrderedSub (ι →₀ α)
Finsupp.instCanonicallyOrderedAddOfAddLeftMono 📋 Mathlib.Data.Finsupp.Order
{ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] [AddLeftMono α] : CanonicallyOrderedAdd (ι →₀ α)
Finsupp.support_tsub 📋 Mathlib.Data.Finsupp.Order
{ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {f1 f2 : ι →₀ α} : (f1 - f2).support ⊆ f1.support

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c