Loogle!

Result

Found 235 declarations mentioning AddLeftStrictMono. Of these, only the first 200 are shown.

AddLeftStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(M : Type u_1) [Add M] [LT M] : Prop
addLeftMono_of_addLeftStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(M : Type u_3) [Add M] [PartialOrder M] [AddLeftStrictMono M] : AddLeftMono M
addRightStrictMono_of_addLeftStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [AddCommSemigroup N] [LT N] [AddLeftStrictMono N] : AddRightStrictMono N
IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [Add N] [IsLeftCancelAdd N] [PartialOrder N] [AddLeftMono N] : AddLeftStrictMono N
addLeftStrictMono_of_addLeftReflectLE 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [Add N] [LinearOrder N] [AddLeftReflectLE N] : AddLeftStrictMono N
AddGroup.addLeftReflectLT_of_addLeftStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
{N : Type u_2} [AddGroup N] [LT N] [AddLeftStrictMono N] : AddLeftReflectLT N
AddLeftStrictMono.toIsLeftCancelAdd 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Add α] [LinearOrder α] [AddLeftStrictMono α] : IsLeftCancelAdd α
add_right_strictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a : α} [Add α] [Preorder α] [AddLeftStrictMono α] : StrictMono fun x => a + x
add_lt_add_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b c : α} [Add α] [LT α] [AddLeftStrictMono α] (bc : b < c) (a : α) : a + b < a + c
StrictAnti.const_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} [AddLeftStrictMono α] (hf : StrictAnti f) (c : α) : StrictAnti fun x => c + f x
StrictMono.const_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} [AddLeftStrictMono α] (hf : StrictMono f) (c : α) : StrictMono fun x => c + f x
addLeftStrictMono_iff_addLeftMono_and_isLeftCancelAdd 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Add α] [LinearOrder α] : AddLeftStrictMono α ↔ AddLeftMono α ∧ IsLeftCancelAdd α
add_lt_add_iff_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b c : α} [Add α] [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (a : α) : a + b < a + c ↔ b < c
StrictAntiOn.const_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [AddLeftStrictMono α] (hf : StrictAntiOn f s) (c : α) : StrictAntiOn (fun x => c + f x) s
StrictMonoOn.const_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [AddLeftStrictMono α] (hf : StrictMonoOn f s) (c : α) : StrictMonoOn (fun x => c + f x) s
add_lt_of_neg_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b : α} [AddZeroClass α] [LT α] [AddLeftStrictMono α] (a : α) (h : b < 0) : a + b < a
lt_add_of_pos_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b : α} [AddZeroClass α] [LT α] [AddLeftStrictMono α] (a : α) (h : 0 < b) : a < a + b
Antitone.add_strictAnti 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] [AddLeftStrictMono α] [AddRightMono α] {f g : β → α} (hf : Antitone f) (hg : StrictAnti g) : StrictAnti fun x => f x + g x
Monotone.add_strictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] [AddLeftStrictMono α] [AddRightMono α] {f g : β → α} (hf : Monotone f) (hg : StrictMono g) : StrictMono fun x => f x + g x
StrictAnti.add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} [AddLeftStrictMono α] [AddRightStrictMono α] (hf : StrictAnti f) (hg : StrictAnti g) : StrictAnti fun x => f x + g x
StrictMono.add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} [AddLeftStrictMono α] [AddRightStrictMono α] (hf : StrictMono f) (hg : StrictMono g) : StrictMono fun x => f x + g x
add_lt_iff_neg_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b : α} [AddZeroClass α] [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (a : α) : a + b < a ↔ b < 0
lt_add_iff_pos_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b : α} [AddZeroClass α] [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (a : α) : a < a + b ↔ 0 < b
add_lt_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] (h₁ : a < b) (h₂ : c < d) : a + c < b + d
add_lt_add_of_le_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [Preorder α] [AddLeftStrictMono α] [AddRightMono α] (h₁ : a ≤ b) (h₂ : c < d) : a + c < b + d
add_lt_add_of_lt_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] (h₁ : a < b) (h₂ : c < d) : a + c < b + d
AntitoneOn.add_strictAnti 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {s : Set β} [AddLeftStrictMono α] [AddRightMono α] {f g : β → α} (hf : AntitoneOn f s) (hg : StrictAntiOn g s) : StrictAntiOn (fun x => f x + g x) s
Left.add_lt_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [Preorder α] [AddLeftStrictMono α] [AddRightMono α] (h₁ : a < b) (h₂ : c < d) : a + c < b + d
MonotoneOn.add_strictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {s : Set β} [AddLeftStrictMono α] [AddRightMono α] {f g : β → α} (hf : MonotoneOn f s) (hg : StrictMonoOn g s) : StrictMonoOn (fun x => f x + g x) s
StrictAntiOn.add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [AddLeftStrictMono α] [AddRightStrictMono α] (hf : StrictAntiOn f s) (hg : StrictAntiOn g s) : StrictAntiOn (fun x => f x + g x) s
StrictMonoOn.add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [AddLeftStrictMono α] [AddRightStrictMono α] (hf : StrictMonoOn f s) (hg : StrictMonoOn g s) : StrictMonoOn (fun x => f x + g x) s
add_lt_of_le_of_neg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] (hbc : b ≤ c) (ha : a < 0) : b + a < c
add_lt_of_lt_of_neg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] (hbc : b < c) (ha : a < 0) : b + a < c
add_neg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] (hbc : b < c) (ha : a < 0) : b + a < c
add_neg_of_nonpos_of_neg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] (hbc : b ≤ c) (ha : a < 0) : b + a < c
add_pos 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] (hbc : b < c) (ha : 0 < a) : b < c + a
add_pos_of_nonneg_of_pos 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] (hbc : b ≤ c) (ha : 0 < a) : b < c + a
add_right_inj_of_comparable 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [Add α] [PartialOrder α] [AddLeftStrictMono α] (h : b ≤ c ∨ c ≤ b) : a + c = a + b ↔ c = b
lt_add_of_le_of_pos 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] (hbc : b ≤ c) (ha : 0 < a) : b < c + a
lt_add_of_lt_of_pos 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] (hbc : b < c) (ha : 0 < a) : b < c + a
Left.add_neg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] (hbc : b < c) (ha : a < 0) : b + a < c
Left.add_neg_of_nonpos_of_neg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] (hbc : b ≤ c) (ha : a < 0) : b + a < c
Left.add_pos 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] (hbc : b < c) (ha : 0 < a) : b < c + a
Left.add_pos_of_nonneg_of_pos 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] (hbc : b ≤ c) (ha : 0 < a) : b < c + a
Left.pos_add_of_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [AddZeroClass α] [Preorder α] [IsBotZeroClass α] [AddLeftStrictMono α] {b : α} (hb : 0 < b) (a : α) : 0 < a + b
add_eq_add_iff_eq_and_eq 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (hac : a ≤ c) (hbd : b ≤ d) : a + b = c + d ↔ a = c ∧ b = d
add_le_add_iff_of_ge 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : a₂ + b₂ ≤ a₁ + b₁ ↔ a₁ = a₂ ∧ b₁ = b₂
cmp_add_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_3} [Add α] [LinearOrder α] [AddLeftStrictMono α] (a b c : α) : cmp (a + b) (a + c) = cmp b c
trichotomy_of_add_eq_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [LinearOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (h : a + b = c + d) : a = c ∧ b = d ∨ a < c ∨ b < d
min_le_max_of_add_le_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [LinearOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (h : a + b ≤ c + d) : min a b ≤ max c d
Left.min_le_max_of_add_le_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [LinearOrder α] [AddLeftStrictMono α] [AddRightMono α] (h : a + b ≤ c + d) : min a b ≤ max c d
sub_lt_self 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] (a : α) {b : α} : 0 < b → a - b < a
sub_lt_self_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] (a : α) {b : α} : a - b < a ↔ 0 < b
neg_lt_self 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [Preorder α] [AddLeftStrictMono α] {a : α} (h : 0 < a) : -a < a
Left.neg_lt_self 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [Preorder α] [AddLeftStrictMono α] {a : α} (h : 0 < a) : -a < a
Left.self_lt_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [Preorder α] [AddLeftStrictMono α] {a : α} (h : a < 0) : a < -a
lt_sub_comm 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : a < b - c ↔ c < b - a
sub_lt_comm 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : a - b < c ↔ a - c < b
lt_neg_of_lt_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] : a < -b → b < -a
lt_of_neg_lt_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] : -a < -b → b < a
neg_lt_of_neg_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] : -a < b → -b < a
neg_of_neg_pos 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} : 0 < -a → a < 0
neg_pos_of_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} : a < 0 → 0 < -a
pos_of_neg_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} : -a < 0 → 0 < a
StrictAnti.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} (hf : StrictAnti f) : StrictMono fun x => -f x
StrictMono.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} (hf : StrictMono f) : StrictAnti fun x => -f x
add_lt_of_lt_sub_left 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : b < c - a → a + b < c
lt_add_of_sub_left_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : a - b < c → a < b + c
lt_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] : a < -b ↔ b < -a
lt_sub_left_of_add_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : a + b < c → b < c - a
neg_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] : -a < b ↔ -b < a
neg_lt_neg_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] : -a < -b ↔ b < a
neg_lt_zero 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} : -a < 0 ↔ 0 < a
neg_neg_iff_pos 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} : -a < 0 ↔ 0 < a
neg_pos 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} : 0 < -a ↔ a < 0
sub_left_lt_of_lt_add 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : a < b + c → a - b < c
Left.neg_neg_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} : -a < 0 ↔ 0 < a
Left.neg_pos_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} : 0 < -a ↔ a < 0
lt_sub_iff_add_lt' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : b < c - a ↔ a + b < c
sub_lt_iff_lt_add' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : a - b < c ↔ a < b + c
sub_lt_sub_left 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] [AddRightStrictMono α] {a b : α} (h : a < b) (c : α) : c - b < c - a
sub_lt_sub_iff_left 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] [AddRightStrictMono α] {b c : α} (a : α) : a - b < a - c ↔ c < b
StrictAntiOn.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} {s : Set β} (hf : StrictAntiOn f s) : StrictMonoOn (fun x => -f x) s
StrictMonoOn.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} {s : Set β} (hf : StrictMonoOn f s) : StrictAntiOn (fun x => -f x) s
lt_neg_add_iff_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} : 0 < -b + a ↔ b < a
lt_neg_iff_add_neg' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} : a < -b ↔ b + a < 0
neg_add_neg_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} : -a + b < 0 ↔ b < a
neg_lt_iff_pos_add' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} : -a < b ↔ 0 < a + b
sub_lt_sub 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [Preorder α] [AddLeftStrictMono α] {a b c d : α} (hab : a < b) (hcd : c < d) : a - d < b - c
add_lt_of_lt_neg_add 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : b < -a + c → a + b < c
lt_add_of_neg_add_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : -b + a < c → a < b + c
lt_add_of_neg_add_lt_left 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : -b + a < c → a < b + c
lt_neg_add_of_add_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : a + b < c → b < -a + c
neg_add_lt_of_lt_add 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : a < b + c → -b + a < c
lt_neg_add_iff_add_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : b < -a + c ↔ a + b < c
neg_add_lt_iff_lt_add 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : -b + a < c ↔ a < b + c
neg_lt_sub_iff_lt_add' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : -b < a - c ↔ c < a + b
add_neg_lt_iff_le_add' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : a + -b < c ↔ a < b + c
neg_add_lt_iff_lt_add' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} : -c + a < b ↔ a < b + c
neg_lt_sub_iff_lt_add 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] [AddRightStrictMono α] {a b c : α} : -a < b - c ↔ c < a + b
sub_lt_sub_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c d : α} : a - b < c - d ↔ a + d < c + b
add_neg_lt_add_neg_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c d : α} : a + -b < c + -d ↔ a + d < c + b
add_neg_lt_neg_add_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c d : α} [AddRightStrictMono α] : a + -b < -d + c ↔ d + a < c + b
lt_iff_exists_pos_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
{α : Type u} [AddZeroClass α] [Preorder α] [ExistsAddOfLE α] {a b : α} [AddLeftStrictMono α] [AddLeftReflectLT α] : a < b ↔ ∃ c, 0 < c ∧ a + c = b
le_iff_forall_pos_le_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
{α : Type u} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [AddLeftReflectLT α] {a b : α} [AddLeftStrictMono α] : a ≤ b ↔ ∀ (ε : α), 0 < ε → a ≤ b + ε
le_iff_forall_pos_lt_add' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
{α : Type u} [LinearOrder α] [DenselyOrdered α] [AddMonoid α] [ExistsAddOfLE α] [AddLeftReflectLT α] {a b : α} [AddLeftStrictMono α] : a ≤ b ↔ ∀ (ε : α), 0 < ε → a < b + ε
lt_add_one 📋 Mathlib.Algebra.Order.Monoid.NatCast
{α : Type u_1} [One α] [AddZeroClass α] [PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftStrictMono α] (a : α) : a < a + 1
one_lt_two 📋 Mathlib.Algebra.Order.Monoid.NatCast
{α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftStrictMono α] : 1 < 2
le_or_le_of_add_le_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Add α] [AddLeftStrictMono α] [AddRightStrictMono α] {a₁ a₂ b₁ b₂ : α} : a₁ + b₁ ≤ a₂ + b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂
lt_or_le_of_add_le_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Add α] [AddLeftStrictMono α] [AddRightMono α] {a₁ a₂ b₁ b₂ : α} : a₁ + b₁ ≤ a₂ + b₂ → a₁ < a₂ ∨ b₁ ≤ b₂
add_lt_add_iff_of_le_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Add α] [AddLeftMono α] [AddRightMono α] [AddLeftStrictMono α] [AddRightStrictMono α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : a₁ + b₁ < a₂ + b₂ ↔ a₁ < a₂ ∨ b₁ < b₂
sub_one_lt 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Ring R] [LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [AddLeftStrictMono R] (a : R) : a - 1 < a
neg_one_lt_zero 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Ring R] [LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [AddLeftStrictMono R] : -1 < 0
lt_two_mul_self 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [PartialOrder R] {a : R} [ZeroLEOneClass R] [MulPosStrictMono R] [NeZero 1] [AddLeftStrictMono R] (ha : 0 < a) : a < 2 * a
mul_add_mul_lt_mul_add_mul 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [PartialOrder R] {a b c d : R} [AddLeftReflectLT R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftStrictMono R] (hab : a < b) (hcd : c < d) : a * d + b * c < a * c + b * d
mul_add_mul_lt_mul_add_mul' 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [PartialOrder R] {a b c d : R} [AddLeftReflectLT R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftStrictMono R] (hba : b < a) (hdc : d < c) : a * d + b * c < a * c + b * d
mul_self_pos 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftStrictMono R] [AddLeftReflectLT R] {a : R} : 0 < a * a ↔ a ≠ 0
mul_pos_iff 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftStrictMono R] [AddLeftReflectLT R] : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
mul_neg_iff 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Ring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftReflectLT R] [AddLeftStrictMono R] : a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
AddMonoidWithOne.toCharZero 📋 Mathlib.Algebra.Order.Ring.Defs
{R : Type u_1} [AddMonoidWithOne R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] [AddLeftStrictMono R] : CharZero R
OrderDual.addLeftStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
{α : Type u} [LT α] [Add α] [c : AddLeftStrictMono α] : AddLeftStrictMono αᵒᵈ
instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] : IsAddTorsionFree M
nsmul_left_strictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] {a : M} (ha : 0 < a) : StrictMono fun x => x • a
nsmul_right_strictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightStrictMono M] {n : ℕ} (hn : n ≠ 0) : StrictMono fun x => n • x
StrictMono.const_nsmul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{β : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [Preorder β] [AddLeftStrictMono M] [AddRightStrictMono M] {f : β → M} (hf : StrictMono f) {n : ℕ} : n ≠ 0 → StrictMono fun x => n • f x
nsmul_lt_nsmul_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] {a : M} {n m : ℕ} (ha : 0 < a) (h : n < m) : n • a < m • a
nsmul_lt_nsmul_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightStrictMono M] {n : ℕ} (hn : n ≠ 0) {a b : M} (hab : a < b) : n • a < n • b
nsmul_le_nsmul_iff_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] {a : M} {m n : ℕ} (ha : 0 < a) : m • a ≤ n • a ↔ m ≤ n
nsmul_lt_nsmul_iff_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] {a : M} {m n : ℕ} (ha : 0 < a) : m • a < n • a ↔ m < n
Left.nsmul_neg_iff 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] {n : ℕ} {x : M} (hn : 0 < n) : n • x < 0 ↔ x < 0
le_of_nsmul_le_nsmul_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b : M} {n : ℕ} (hn : n ≠ 0) : n • a ≤ n • b → a ≤ b
nsmul_le_nsmul_iff_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b : M} {n : ℕ} (hn : n ≠ 0) : n • a ≤ n • b ↔ a ≤ b
le_max_of_two_nsmul_le_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b c : M} (h : 2 • a ≤ b + c) : a ≤ max b c
min_le_of_add_le_two_nsmul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b c : M} (h : a + b ≤ 2 • c) : min a b ≤ c
exists_lt_nsmul 📋 Mathlib.Algebra.Order.Archimedean.Defs
{R : Type u_1} [AddCommMonoid R] [PartialOrder R] [AddLeftStrictMono R] [Archimedean R] {a : R} (ha : 0 < a) (b : R) : ∃ n, b < n • a
lt_iff_exists_add 📋 Mathlib.Algebra.Order.Monoid.Canonical.Defs
{α : Type u} [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] {a b : α} [AddLeftStrictMono α] : a < b ↔ ∃ c > 0, b = a + c
WithBot.add_lt_add_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddLeftStrictMono α] (hx : x ≠ ⊥) : y < z → x + y < x + z
WithTop.add_lt_add_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddLeftStrictMono α] (hx : x ≠ ⊤) : y < z → x + y < x + z
WithBot.add_lt_add_iff_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (hx : x ≠ ⊥) : x + y < x + z ↔ y < z
WithTop.add_lt_add_iff_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (hx : x ≠ ⊤) : x + y < x + z ↔ y < z
WithTop.add_lt_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {w x y z : WithTop α} [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] (xz : x < z) (yw : y < w) : x + y < z + w
WithBot.add_lt_add_of_le_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {w x y z : WithBot α} [Preorder α] [AddLeftStrictMono α] [AddRightMono α] (hw : w ≠ ⊥) (hwy : w ≤ y) (hxz : x < z) : w + x < y + z
WithTop.add_lt_add_of_le_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {w x y z : WithTop α} [Preorder α] [AddLeftStrictMono α] [AddRightMono α] (hw : w ≠ ⊤) (hwy : w ≤ y) (hxz : x < z) : w + x < y + z
OrderEmbedding.addLeft 📋 Mathlib.Algebra.Order.Monoid.Basic
{α : Type u_2} [Add α] [LinearOrder α] [AddLeftStrictMono α] (m : α) : α ↪o α
OrderEmbedding.addLeft_apply 📋 Mathlib.Algebra.Order.Monoid.Basic
{α : Type u_2} [Add α] [LinearOrder α] [AddLeftStrictMono α] (m n : α) : (OrderEmbedding.addLeft m) n = m + n
Positive.addSemigroup 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] : AddSemigroup { x // 0 < x }
Positive.instAddSubtypeLtOfNat_mathlib 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] : Add { x // 0 < x }
Positive.addCommSemigroup 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_3} [AddCommMonoid M] [Preorder M] [AddLeftStrictMono M] : AddCommSemigroup { x // 0 < x }
Positive.addLeftCancelSemigroup 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_3} [AddLeftCancelMonoid M] [Preorder M] [AddLeftStrictMono M] : AddLeftCancelSemigroup { x // 0 < x }
Positive.addRightCancelSemigroup 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_3} [AddRightCancelMonoid M] [Preorder M] [AddLeftStrictMono M] : AddRightCancelSemigroup { x // 0 < x }
Positive.addLeftStrictMono 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] : AddLeftStrictMono { x // 0 < x }
Positive.addLeftMono 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_1} [AddMonoid M] [PartialOrder M] [AddLeftStrictMono M] : AddLeftMono { x // 0 < x }
Positive.addLeftReflectLE 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddLeftReflectLE M] : AddLeftReflectLE { x // 0 < x }
Positive.addLeftReflectLT 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddLeftReflectLT M] : AddLeftReflectLT { x // 0 < x }
Positive.addRightReflectLE 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightReflectLE M] : AddRightReflectLE { x // 0 < x }
Positive.addRightReflectLT 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightReflectLT M] : AddRightReflectLT { x // 0 < x }
Positive.addRightStrictMono 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightStrictMono M] : AddRightStrictMono { x // 0 < x }
Positive.coe_add 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] (x y : { x // 0 < x }) : ↑(x + y) = ↑x + ↑y
instAddLeftStrictMonoPNat 📋 Mathlib.Data.PNat.Basic
: AddLeftStrictMono ℕ+
List.sum_lt_sum_of_ne_nil 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{ι : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddLeftMono M] [AddRightStrictMono M] [AddRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M) (hlt : ∀ i ∈ l, f i < g i) : (List.map f l).sum < (List.map g l).sum
List.sum_lt_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{ι : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddLeftMono M] [AddRightStrictMono M] [AddRightMono M] {l : List ι} (f g : ι → M) (h₁ : ∀ i ∈ l, f i ≤ g i) (h₂ : ∃ i ∈ l, f i < g i) : (List.map f l).sum < (List.map g l).sum
List.exists_le_of_sum_le 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{ι : Type u_1} {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddLeftMono M] [AddRightStrictMono M] [AddRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M) (h : (List.map f l).sum ≤ (List.map g l).sum) : ∃ x ∈ l, f x ≤ g x
Finset.sum_erase_lt_of_pos 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_5} [DecidableEq ι] [AddCommMonoid κ] [LT κ] [AddLeftStrictMono κ] {s : Finset ι} {d : ι} (hd : d ∈ s) {f : ι → κ} (hdf : 0 < f d) : ∑ m ∈ s.erase d, f m < ∑ m ∈ s, f m
Multiset.sum_lt_sum_of_nonempty 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
{ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [Preorder α] [IsOrderedCancelAddMonoid α] [AddLeftStrictMono α] {s : Multiset ι} {f g : ι → α} (hs : s ≠ ∅) (hfg : ∀ i ∈ s, f i < g i) : (Multiset.map f s).sum < (Multiset.map g s).sum
Multiset.sum_lt_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
{ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [Preorder α] [IsOrderedCancelAddMonoid α] [AddLeftStrictMono α] {s : Multiset ι} {f g : ι → α} (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) : (Multiset.map f s).sum < (Multiset.map g s).sum
Finset.sum_lt_sum_of_nonempty 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Preorder M] [IsOrderedCancelAddMonoid M] {f g : ι → M} {s : Finset ι} [AddLeftStrictMono M] (hs : s.Nonempty) (hlt : ∀ i ∈ s, f i < g i) : ∑ i ∈ s, f i < ∑ i ∈ s, g i
Finset.sum_neg 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s : Finset ι} [AddLeftStrictMono M] (h : ∀ i ∈ s, f i < 0) (hs : s.Nonempty) : ∑ i ∈ s, f i < 0
Finset.sum_pos 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s : Finset ι} [AddLeftStrictMono M] (h : ∀ i ∈ s, 0 < f i) (hs : s.Nonempty) : 0 < ∑ i ∈ s, f i
Finset.sum_lt_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Preorder M] [IsOrderedCancelAddMonoid M] {f g : ι → M} {s : Finset ι} [AddLeftStrictMono M] (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) : ∑ i ∈ s, f i < ∑ i ∈ s, g i
Finset.sum_lt_sum_of_subset_erase_union_singleton 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{ι : Type u_8} {M : Type u_9} [DecidableEq ι] [AddCommMonoid M] [PartialOrder M] [CanonicallyOrderedAdd M] [AddLeftStrictMono M] {S S' : Finset ι} {f : ι → M} {d d' : ι} (hd_mem : d ∈ S) (hS' : S' ⊆ S.erase d ∪ {d'}) (hlt : f d' < f d) : ∑ x ∈ S', f x < ∑ x ∈ S, f x
Finset.sum_neg' 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s : Finset ι} [AddLeftStrictMono M] (h : ∀ i ∈ s, f i ≤ 0) (hs : ∃ i ∈ s, f i < 0) : ∑ i ∈ s, f i < 0
Finset.sum_pos' 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s : Finset ι} [AddLeftStrictMono M] (h : ∀ i ∈ s, 0 ≤ f i) (hs : ∃ i ∈ s, 0 < f i) : 0 < ∑ i ∈ s, f i
Finset.single_lt_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s : Finset ι} [AddLeftStrictMono M] {i j : ι} (hij : j ≠ i) (hi : i ∈ s) (hj : j ∈ s) (hlt : 0 < f j) (hle : ∀ k ∈ s, k ≠ i → 0 ≤ f k) : f i < ∑ k ∈ s, f k
Finset.sum_lt_sum_of_subset 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s t : Finset ι} [AddLeftStrictMono M] (h : s ⊆ t) {i : ι} (ht : i ∈ t) (hs : i ∉ s) (hlt : 0 < f i) (hle : ∀ j ∈ t, j ∉ s → 0 ≤ f j) : ∑ j ∈ s, f j < ∑ j ∈ t, f j
Ordinal.instAddLeftStrictMono 📋 Mathlib.SetTheory.Ordinal.Arithmetic
: AddLeftStrictMono Ordinal.{u}
TwoUniqueSums.of_covariant_right 📋 Mathlib.Algebra.Group.UniqueProds.Basic
{G : Type u} [Add G] [IsRightCancelAdd G] [LinearOrder G] [AddLeftStrictMono G] : TwoUniqueSums G
AddMonoidAlgebra.Monic.mul 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hp : AddMonoidAlgebra.Monic D p) (hq : AddMonoidAlgebra.Monic D q) : AddMonoidAlgebra.Monic D (p * q)
AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_left 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hq : AddMonoidAlgebra.Monic D q) : AddMonoidAlgebra.leadingCoeff D (p * q) = AddMonoidAlgebra.leadingCoeff D p
AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_right 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hp : AddMonoidAlgebra.Monic D p) : AddMonoidAlgebra.leadingCoeff D (p * q) = AddMonoidAlgebra.leadingCoeff D q
AddMonoidAlgebra.Monic.pow 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} [Semiring R] {A : Type u_8} {B : Type u_9} [AddMonoid A] [AddMonoid B] [LinearOrder B] [OrderBot B] [AddLeftStrictMono B] [AddRightStrictMono B] {D : A → B} {p : AddMonoidAlgebra R A} {n : ℕ} (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hD : Function.Injective D) (hp : AddMonoidAlgebra.Monic D p) : AddMonoidAlgebra.Monic D (p ^ n)
AddMonoidAlgebra.leadingCoeff_mul 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] [NoZeroDivisors R] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) : AddMonoidAlgebra.leadingCoeff D (p * q) = AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q
AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hq : AddMonoidAlgebra.Monic D q) (hp : p ≠ 0) : AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_right 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hp : AddMonoidAlgebra.Monic D p) (hq : q ≠ 0) : AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
AddMonoidAlgebra.Monic.supDegree_pow 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} [Semiring R] {A : Type u_8} {B : Type u_9} [AddMonoid A] [AddMonoid B] [LinearOrder B] [OrderBot B] [AddLeftStrictMono B] [AddRightStrictMono B] {D : A → B} {p : AddMonoidAlgebra R A} {n : ℕ} (hzero : D 0 = 0) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hD : Function.Injective D) [Nontrivial R] (hp : AddMonoidAlgebra.Monic D p) : AddMonoidAlgebra.supDegree D (p ^ n) = n • AddMonoidAlgebra.supDegree D p
AddMonoidAlgebra.apply_supDegree_add_supDegree 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) : (p * q).coeff (Function.invFun D (AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q)) = AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q
AddMonoidAlgebra.coeff_supDegree_add_supDegree 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) : (p * q).coeff (Function.invFun D (AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q)) = AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q
AddMonoidAlgebra.apply_add_of_supDegree_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} {p q : AddMonoidAlgebra R A} [AddZeroClass A] [Add B] (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) {ap aq : A} (hp : AddMonoidAlgebra.supDegree D p ≤ D ap) (hq : AddMonoidAlgebra.supDegree D q ≤ D aq) : (p * q).coeff (ap + aq) = p.coeff ap * q.coeff aq
AddMonoidAlgebra.coeff_add_of_supDegree_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} {p q : AddMonoidAlgebra R A} [AddZeroClass A] [Add B] (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) {ap aq : A} (hp : AddMonoidAlgebra.supDegree D p ≤ D ap) (hq : AddMonoidAlgebra.supDegree D q ≤ D aq) : (p * q).coeff (ap + aq) = p.coeff ap * q.coeff aq
AddMonoidAlgebra.Monic.supDegree_mul 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hbot : ⊥ + ⊥ = ⊥) (hp : AddMonoidAlgebra.Monic D p) (hq : AddMonoidAlgebra.Monic D q) : AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
AddMonoidAlgebra.supDegree_mul 📋 Mathlib.Algebra.MonoidAlgebra.Degree
{R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hpq : AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q ≠ 0) (hp : p ≠ 0) (hq : q ≠ 0) : AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
Finsupp.sum_pos 📋 Mathlib.Data.Finsupp.Order
{ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [AddCommMonoid β] [Preorder β] [IsOrderedCancelAddMonoid β] [AddLeftStrictMono β] {f : ι →₀ α} {g : ι → α → β} (h : ∀ i ∈ f.support, 0 < g i (f i)) (hf : f ≠ 0) : 0 < f.sum g
Finsupp.sum_pos' 📋 Mathlib.Data.Finsupp.Order
{ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [AddCommMonoid β] [Preorder β] [IsOrderedCancelAddMonoid β] [AddLeftStrictMono β] {f : ι →₀ α} {g : ι → α → β} (h : ∀ i ∈ f.support, 0 ≤ g i (f i)) (hf : ∃ i ∈ f.support, 0 < g i (f i)) : 0 < f.sum g
DFinsupp.Colex.addLeftStrictMono 📋 Mathlib.Data.DFinsupp.Lex
{ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)] : AddLeftStrictMono (Colex (Π₀ (i : ι), α i))
DFinsupp.Lex.addLeftStrictMono 📋 Mathlib.Data.DFinsupp.Lex
{ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)] : AddLeftStrictMono (Lex (Π₀ (i : ι), α i))
DFinsupp.Colex.addLeftMono 📋 Mathlib.Data.DFinsupp.Lex
{ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)] : AddLeftMono (Colex (Π₀ (i : ι), α i))
DFinsupp.Lex.addLeftMono 📋 Mathlib.Data.DFinsupp.Lex
{ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)] : AddLeftMono (Lex (Π₀ (i : ι), α i))
Finsupp.Colex.addLeftStrictMono 📋 Mathlib.Data.Finsupp.Lex
{α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddLeftStrictMono N] : AddLeftStrictMono (Colex (α →₀ N))
Finsupp.Lex.addLeftStrictMono 📋 Mathlib.Data.Finsupp.Lex
{α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddLeftStrictMono N] : AddLeftStrictMono (Lex (α →₀ N))
Finsupp.Colex.addLeftMono 📋 Mathlib.Data.Finsupp.Lex
{α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddLeftStrictMono N] : AddLeftMono (Colex (α →₀ N))
Finsupp.Lex.addLeftMono 📋 Mathlib.Data.Finsupp.Lex
{α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddLeftStrictMono N] : AddLeftMono (Lex (α →₀ N))

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