Loogle!
Result
Found 392 declarations mentioning AddRightMono. Of these, only the first 200 are shown.
- AddRightMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(M : Type u_1) [Add M] [LE M] : Prop - addRightMono_of_addLeftMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [AddCommSemigroup N] [LE N] [AddLeftMono N] : AddRightMono N - addRightMono_of_addRightStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(M : Type u_3) [Add M] [PartialOrder M] [AddRightStrictMono M] : AddRightMono M - IsRightCancelAdd.addRightStrictMono_of_addRightMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [Add N] [IsRightCancelAdd N] [PartialOrder N] [AddRightMono N] : AddRightStrictMono N - addRightReflectLT_of_addRightMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [Add N] [LinearOrder N] [AddRightMono N] : AddRightReflectLT N - AddGroup.addRightReflectLE_of_addRightMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
{N : Type u_2} [AddGroup N] [LE N] [AddRightMono N] : AddRightReflectLE N - add_left_mono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a : α} [Add α] [Preorder α] [AddRightMono α] : Monotone fun x => x + a - add_le_add_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b c : α} [Add α] [LE α] [i : AddRightMono α] (bc : b ≤ c) (a : α) : b + a ≤ c + a - Antitone.add_const 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} [AddRightMono α] (hf : Antitone f) (a : α) : Antitone fun x => f x + a - Monotone.add_const 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} [AddRightMono α] (hf : Monotone f) (a : α) : Monotone fun x => f x + a - addRightStrictMono_iff_addRightMono_and_isRightCancelAdd 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Add α] [LinearOrder α] : AddRightStrictMono α ↔ AddRightMono α ∧ IsRightCancelAdd α - add_le_add_iff_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b c : α} [Add α] [LE α] [AddRightMono α] [AddRightReflectLE α] (a : α) : b + a ≤ c + a ↔ b ≤ c - AntitoneOn.add_const 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [AddRightMono α] (hf : AntitoneOn f s) (a : α) : AntitoneOn (fun x => f x + a) s - MonotoneOn.add_const 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [AddRightMono α] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => f x + a) s - add_le_of_nonpos_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [AddZeroClass α] [LE α] [AddRightMono α] (h : b ≤ 0) : b + a ≤ a - le_add_of_nonneg_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [AddZeroClass α] [LE α] [AddRightMono α] (h : 0 ≤ b) : a ≤ b + a - add_le_of_add_le_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [Preorder α] [AddRightMono α] (h : a + b ≤ c) (hle : d ≤ a) : d + b ≤ c - add_lt_of_add_lt_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [Preorder α] [AddRightMono α] (h : a + b < c) (hle : d ≤ a) : d + b < c - le_add_of_le_add_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [Preorder α] [AddRightMono α] (h : a ≤ b + c) (hle : b ≤ d) : a ≤ d + c - lt_add_of_lt_add_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [Preorder α] [AddRightMono α] (h : a < b + c) (hle : b ≤ d) : a < d + c - Antitone.add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} [AddLeftMono α] [AddRightMono α] (hf : Antitone f) (hg : Antitone g) : Antitone fun x => f x + g x - 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 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} [AddLeftMono α] [AddRightMono α] (hf : Monotone f) (hg : Monotone g) : Monotone 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 - add_le_iff_nonpos_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [AddZeroClass α] [LE α] [AddRightMono α] [AddRightReflectLE α] : a + b ≤ b ↔ a ≤ 0 - le_add_iff_nonneg_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b : α} [AddZeroClass α] [LE α] [AddRightMono α] [AddRightReflectLE α] (a : α) : a ≤ b + a ↔ 0 ≤ b - add_le_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [Preorder α] [AddLeftMono α] [AddRightMono α] (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 - AntitoneOn.add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [AddLeftMono α] [AddRightMono α] (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => f x + g x) s - 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 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [AddLeftMono α] [AddRightMono α] (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => f x + g x) s - 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 - add_le_of_nonpos_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (ha : a ≤ 0) (hbc : b ≤ c) : a + b ≤ c - add_lt_of_neg_of_lt' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (ha : a < 0) (hbc : b < c) : a + b < c - add_lt_of_nonpos_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (ha : a ≤ 0) (hbc : b < c) : a + b < c - le_add_of_nonneg_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (ha : 0 ≤ a) (hbc : b ≤ c) : b ≤ a + c - le_of_add_le_of_nonneg_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (h : a + b ≤ c) (hle : 0 ≤ a) : b ≤ c - le_of_le_add_of_nonpos_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (h : a ≤ b + c) (hle : b ≤ 0) : a ≤ c - lt_add_of_nonneg_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (ha : 0 ≤ a) (hbc : b < c) : b < a + c - lt_add_of_pos_of_lt' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (ha : 0 < a) (hbc : b < c) : b < a + c - lt_of_add_lt_of_nonneg_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (h : a + b < c) (hle : 0 ≤ a) : b < c - lt_of_lt_add_of_nonpos_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (h : a < b + c) (hle : b ≤ 0) : a < c - Right.add_neg' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (ha : a < 0) (hbc : b < c) : a + b < c - Right.add_neg_of_nonpos_of_neg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (ha : a ≤ 0) (hbc : b < c) : a + b < c - Right.add_nonneg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (ha : 0 ≤ a) (hbc : b ≤ c) : b ≤ a + c - Right.add_nonpos 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (ha : a ≤ 0) (hbc : b ≤ c) : a + b ≤ c - Right.add_pos' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (ha : 0 < a) (hbc : b < c) : b < a + c - Right.add_pos_of_nonneg_of_pos 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightMono α] (ha : 0 ≤ a) (hbc : b < c) : b < a + c - add_pos_of_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [AddZeroClass α] [Preorder α] [IsBotZeroClass α] [AddRightMono α] {b : α} (hb : 0 < b) (a : α) : 0 < a + b - Right.pos_add_of_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [AddZeroClass α] [Preorder α] [IsBotZeroClass α] [AddRightMono α] {b : α} (hb : 0 < b) (a : α) : 0 < a + b - max_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Add α] [LinearOrder α] [AddRightMono α] (a b c : α) : max a b + c = max (a + c) (b + c) - min_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Add α] [LinearOrder α] [AddRightMono α] (a b c : α) : min a b + c = min (a + c) (b + c) - add_le_add_three 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d e f : α} [Add α] [Preorder α] [AddLeftMono α] [AddRightMono α] (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : a + b + c ≤ d + e + f - eq_zero_of_add_nonneg_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [AddZeroClass α] [PartialOrder α] [AddRightMono α] (ha : a ≤ 0) (hb : b ≤ 0) (hab : 0 ≤ a + b) : b = 0 - eq_zero_of_add_nonpos_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [AddZeroClass α] [PartialOrder α] [AddRightMono α] (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 0) : b = 0 - min_lt_max_of_add_lt_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [LinearOrder α] [AddLeftMono α] [AddRightMono α] (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 - max_add_add_le_max_add_max 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [LinearOrder α] [AddLeftMono α] [AddRightMono α] : max (a + b) (c + d) ≤ max a c + max b d - min_add_min_le_min_add_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Add α] [LinearOrder α] [AddLeftMono α] [AddRightMono α] : min a c + min b d ≤ min (a + b) (c + d) - add_eq_zero_iff_of_nonneg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [AddZeroClass α] [PartialOrder α] [AddLeftMono α] [AddRightMono α] (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 - AddGroup.toOrderedSub 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u_1} [AddGroup α] [LE α] [AddRightMono α] : OrderedSub α - le_of_sub_nonneg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} : 0 ≤ a - b → b ≤ a - le_of_sub_nonpos 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} : a - b ≤ 0 → a ≤ b - sub_le_sub_right 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} (h : a ≤ b) (c : α) : a - c ≤ b - c - sub_nonneg_of_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} : b ≤ a → 0 ≤ a - b - sub_nonpos_of_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} : a ≤ b → a - b ≤ 0 - sub_le_sub_iff_right 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} (c : α) : a - c ≤ b - c ↔ a ≤ b - sub_nonneg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} : 0 ≤ a - b ↔ b ≤ a - sub_nonpos 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} : a - b ≤ 0 ↔ a ≤ b - Right.neg_le_self 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [Preorder α] [AddRightMono α] {a : α} (h : 0 ≤ a) : -a ≤ a - Right.self_le_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [Preorder α] [AddRightMono α] {a : α} (h : a ≤ 0) : a ≤ -a - add_le_of_le_sub_right 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b c : α} : a ≤ c - b → a + b ≤ c - le_sub_right_of_add_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b c : α} : a + b ≤ c → a ≤ c - b - le_sub_iff_add_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b c : α} : a ≤ c - b ↔ a + b ≤ c - sub_le_iff_le_add 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b c : α} : a - c ≤ b ↔ a ≤ b + c - le_of_neg_le_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b : α} [AddRightMono α] : -a ≤ -b → b ≤ a - Antitone.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftMono α] [AddRightMono α] [Preorder β] {f : β → α} (hf : Antitone f) : Monotone fun x => -f x - Monotone.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftMono α] [AddRightMono α] [Preorder β] {f : β → α} (hf : Monotone f) : Antitone fun x => -f x - neg_le_neg_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b : α} [AddRightMono α] : -a ≤ -b ↔ b ≤ a - Right.neg_nonpos_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a : α} : -a ≤ 0 ↔ 0 ≤ a - Right.nonneg_neg_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a : α} : 0 ≤ -a ↔ a ≤ 0 - sub_le_sub_left 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {a b : α} (h : a ≤ b) (c : α) : c - b ≤ c - a - sub_le_sub_iff_left 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {b c : α} (a : α) : a - b ≤ a - c ↔ c ≤ b - AntitoneOn.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftMono α] [AddRightMono α] [Preorder β] {f : β → α} {s : Set β} (hf : AntitoneOn f s) : MonotoneOn (fun x => -f x) s - MonotoneOn.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftMono α] [AddRightMono α] [Preorder β] {f : β → α} {s : Set β} (hf : MonotoneOn f s) : AntitoneOn (fun x => -f x) s - add_neg_nonpos_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} : b + -a ≤ 0 ↔ b ≤ a - add_neg_nonpos_iff_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} : a + -b ≤ 0 ↔ a ≤ b - le_add_neg_iff_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} : 0 ≤ a + -b ↔ b ≤ a - le_neg_iff_add_nonpos_right 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} : a ≤ -b ↔ a + b ≤ 0 - neg_le_iff_add_nonneg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} : -a ≤ b ↔ 0 ≤ b + a - add_neg_le_iff_le_add 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b c : α} : a + -b ≤ c ↔ a ≤ c + b - le_add_neg_iff_add_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b c : α} : c ≤ a + -b ↔ c + b ≤ a - cmp_sub_zero 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LinearOrder α] [AddRightMono α] (a b : α) : cmp (a - b) 0 = cmp a b - sub_le_neg_add_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a b : α} [AddRightMono α] : a - b ≤ -a + b ↔ a ≤ b - add_neg_le_neg_add_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b c d : α} [AddRightMono α] : a + -b ≤ -d + c ↔ d + a ≤ c + b - one_le_two' 📋 Mathlib.Algebra.Order.Monoid.NatCast
{α : Type u_1} [AddMonoidWithOne α] [LE α] [ZeroLEOneClass α] [AddRightMono α] : 1 ≤ 2 - max_add_add_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Add α] [AddRightMono α] (a b c : α) : max (a + c) (b + c) = max a b + c - min_add_add_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Add α] [AddRightMono α] (a b c : α) : min (a + c) (b + c) = min a b + c - min_le_add_of_nonneg_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [AddZeroClass α] [AddRightMono α] {a b : α} (ha : 0 ≤ a) : min a b ≤ a + 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₂ - lt_or_lt_of_add_lt_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Add α] [AddLeftMono α] [AddRightMono α] {a₁ a₂ b₁ b₂ : α} : a₁ + b₁ < a₂ + b₂ → a₁ < a₂ ∨ b₁ < b₂ - max_le_add_of_nonneg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [AddZeroClass α] [AddLeftMono α] [AddRightMono α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : max a b ≤ a + 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₂ - antitone_mul_left 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] {a : R} (ha : a ≤ 0) : Antitone fun x => a * x - antitone_mul_right 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] {a : R} (ha : a ≤ 0) : Antitone fun x => x * a - Antitone.const_mul_of_nonpos 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} {α : Type u_1} [Semiring R] [Preorder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Antitone f) (ha : a ≤ 0) : Monotone fun x => a * f x - Antitone.mul_const_of_nonpos 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} {α : Type u_1} [Semiring R] [Preorder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Antitone f) (ha : a ≤ 0) : Monotone fun x => f x * a - Monotone.const_mul_of_nonpos 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} {α : Type u_1} [Semiring R] [Preorder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Monotone f) (ha : a ≤ 0) : Antitone fun x => a * f x - Monotone.mul_const_of_nonpos 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} {α : Type u_1} [Semiring R] [Preorder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Monotone f) (ha : a ≤ 0) : Antitone fun x => f x * a - le_mul_of_le_one_left 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] {a b : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hb : b ≤ 0) (h : a ≤ 1) : b ≤ a * b - le_mul_of_le_one_right 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] {a b : R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (ha : a ≤ 0) (h : b ≤ 1) : a ≤ a * b - mul_le_mul_of_nonpos_left 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] {a b c : R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (h : b ≤ a) (hc : c ≤ 0) : c * a ≤ c * b - mul_le_mul_of_nonpos_right 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] {a b c : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c - mul_le_of_one_le_left 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] {a b : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hb : b ≤ 0) (h : 1 ≤ a) : a * b ≤ b - mul_le_of_one_le_right 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] {a b : R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (ha : a ≤ 0) (h : 1 ≤ b) : a * b ≤ a - mul_nonneg_of_nonpos_of_nonpos 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] {a b : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b - mul_le_mul_of_nonneg_of_nonpos 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hbd : b ≤ d) (hc : 0 ≤ c) (hb : b ≤ 0) : a * b ≤ c * d - mul_le_mul_of_nonneg_of_nonpos' 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] {a b c d : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hbd : b ≤ d) (ha : 0 ≤ a) (hd : d ≤ 0) : a * b ≤ c * d - mul_le_mul_of_nonpos_of_nonneg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hac : a ≤ c) (hdb : d ≤ b) (hc : c ≤ 0) (hb : 0 ≤ b) : a * b ≤ c * d - mul_le_mul_of_nonpos_of_nonneg' 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] {a b c d : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hbd : b ≤ d) (ha : 0 ≤ a) (hd : d ≤ 0) : a * b ≤ c * d - mul_le_mul_of_nonpos_of_nonpos 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hdb : d ≤ b) (hc : c ≤ 0) (hb : b ≤ 0) : a * b ≤ c * d - mul_le_mul_of_nonpos_of_nonpos' 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [Preorder R] {a b c d : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hdb : d ≤ b) (ha : a ≤ 0) (hd : d ≤ 0) : a * b ≤ c * d - Antitone.mul 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} {α : Type u_1} [Semiring R] [Preorder R] [Preorder α] {f g : α → R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Antitone f) (hg : Antitone g) (hf₀ : ∀ (x : α), f x ≤ 0) (hg₀ : ∀ (x : α), g x ≤ 0) : Monotone (f * g) - Antitone.mul_monotone 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} {α : Type u_1} [Semiring R] [Preorder R] [Preorder α] {f g : α → R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Antitone f) (hg : Monotone g) (hf₀ : ∀ (x : α), f x ≤ 0) (hg₀ : ∀ (x : α), 0 ≤ g x) : Antitone (f * g) - Monotone.mul_antitone 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} {α : Type u_1} [Semiring R] [Preorder R] [Preorder α] {f g : α → R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Monotone f) (hg : Antitone g) (hf₀ : ∀ (x : α), 0 ≤ f x) (hg₀ : ∀ (x : α), g x ≤ 0) : Antitone (f * g) - lt_of_mul_lt_mul_of_nonpos_left 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] {a b c : R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (h : c * a < c * b) (hc : c ≤ 0) : b < a - lt_of_mul_lt_mul_of_nonpos_right 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] {a b c : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (h : a * c < b * c) (hc : c ≤ 0) : b < a - pos_of_right_mul_lt_le 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] {a b c : R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (h : a * b < a * c) (hbc : b ≤ c) : 0 < a - mul_le_mul_left_of_neg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightMono R] [AddRightReflectLE R] {a b c : R} (h : c < 0) : c * a ≤ c * b ↔ b ≤ a - mul_le_mul_right_of_neg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightMono R] [AddRightReflectLE R] {a b c : R} (h : c < 0) : a * c ≤ b * c ↔ b ≤ a - nonneg_of_mul_nonpos_left 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightMono R] [AddRightReflectLE R] {a b : R} (h : a * b ≤ 0) (hb : b < 0) : 0 ≤ a - nonneg_of_mul_nonpos_right 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightMono R] [AddRightReflectLE R] {a b : R} (h : a * b ≤ 0) (ha : a < 0) : 0 ≤ b - pos_of_mul_neg_left 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] {a b : R} (h : a * b < 0) (hb : b ≤ 0) : 0 < a - pos_of_mul_neg_right 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] {a b : R} (h : a * b < 0) (ha : a ≤ 0) : 0 < b - neg_iff_pos_of_mul_neg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hab : a * b < 0) : a < 0 ↔ 0 < b - pos_iff_neg_of_mul_neg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hab : a * b < 0) : 0 < a ↔ b < 0 - IsOrderedAddMonoid.toAddRightMono 📋 Mathlib.Algebra.Order.Monoid.Defs
{α : Type u_1} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] : AddRightMono α - OrderIso.addRight 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a : α) : α ≃o α - OrderIso.subRight 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a : α) : α ≃o α - OrderIso.neg 📋 Mathlib.Algebra.Order.Group.OrderIso
(α : Type u) [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] : α ≃o αᵒᵈ - OrderIso.subLeft 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a : α) : α ≃o αᵒᵈ - OrderIso.addRight_toEquiv 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a : α) : (OrderIso.addRight a).toEquiv = Equiv.addRight a - OrderIso.addRight_symm 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a : α) : (OrderIso.addRight a).symm = OrderIso.addRight (-a) - le_neg_of_le_neg 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {a b : α} : a ≤ -b → b ≤ -a - neg_le_of_neg_le 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {a b : α} : -a ≤ b → -b ≤ a - le_neg 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {a b : α} : a ≤ -b ↔ b ≤ -a - neg_le 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {a b : α} : -a ≤ b ↔ -b ≤ a - OrderIso.subRight_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a b : α) : (OrderIso.subRight a) b = b - a - OrderIso.addRight_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a x : α) : (OrderIso.addRight a) x = x + a - OrderIso.subRight_symm_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a b : α) : (RelIso.symm (OrderIso.subRight a)) b = b + a - OrderIso.neg_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
(α : Type u) [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a✝ : α) : (OrderIso.neg α) a✝ = OrderDual.toDual (-a✝) - OrderIso.subLeft_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a a✝ : α) : (OrderIso.subLeft a) a✝ = OrderDual.toDual (a - a✝) - OrderIso.neg_symm_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
(α : Type u) [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a✝ : αᵒᵈ) : (RelIso.symm (OrderIso.neg α)) a✝ = -OrderDual.ofDual a✝ - OrderIso.subLeft_symm_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a : α) (a✝ : αᵒᵈ) : (RelIso.symm (OrderIso.subLeft a)) a✝ = -OrderDual.ofDual a✝ + a - OrderDual.addRightMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
{α : Type u} [LE α] [Add α] [c : AddRightMono α] : AddRightMono αᵒᵈ - nsmul_right_mono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] [AddRightMono M] (n : ℕ) : Monotone fun a => n • a - Monotone.const_nsmul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{β : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [Preorder β] [AddLeftMono M] [AddRightMono M] {f : β → M} (hf : Monotone f) (n : ℕ) : Monotone fun a => n • f a - Right.nsmul_nonneg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] {x : M} (hx : 0 ≤ x) {n : ℕ} : 0 ≤ n • x - Right.nsmul_nonpos 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] {x : M} (hx : x ≤ 0) {n : ℕ} : n • x ≤ 0 - nsmul_le_nsmul_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] [AddRightMono M] {a b : M} (hab : a ≤ b) (i : ℕ) : i • a ≤ i • b - Right.nsmul_neg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] {n : ℕ} {x : M} (hn : 0 < n) (h : x < 0) : n • x < 0 - nsmul_le_nsmul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] [AddRightMono M] {a b : M} (hab : a ≤ b) (ht : 0 ≤ b) {m n : ℕ} (hmn : m ≤ n) : m • a ≤ n • b - lt_of_nsmul_lt_nsmul_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftMono M] [AddRightMono M] {a b : M} (n : ℕ) : n • a < n • b → a < b - lt_max_of_two_nsmul_lt_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftMono M] [AddRightMono M] {a b c : M} (h : 2 • a < b + c) : a < max b c - min_lt_of_add_lt_two_nsmul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftMono M] [AddRightMono M] {a b c : M} (h : a + b < 2 • c) : min a b < c - nsmul_le_nsmul_add_of_sq_le_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] {a b : M} (hab : 2 • a ≤ b + a) {n : ℕ} : n ≠ 0 → n • a ≤ (n - 1) • b + a - inf_sub 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [AddGroup α] [AddRightMono α] (a b c : α) : a ⊓ b - c = (a - c) ⊓ (b - c) - sup_sub 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [AddGroup α] [AddRightMono α] (a b c : α) : a ⊔ b - c = (a - c) ⊔ (b - c) - inf_add 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [AddGroup α] [AddRightMono α] (a b c : α) : a ⊓ b + c = (a + c) ⊓ (b + c) - neg_inf 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a b : α) : -(a ⊓ b) = -a ⊔ -b - neg_sup 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a b : α) : -(a ⊔ b) = -a ⊓ -b - sup_add 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [AddGroup α] [AddRightMono α] (a b c : α) : a ⊔ b + c = (a + c) ⊔ (b + c) - sub_inf 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a b c : α) : c - a ⊓ b = (c - a) ⊔ (c - b) - sub_sup 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a b c : α) : c - a ⊔ b = (c - a) ⊓ (c - b) - nsmul_two_semiclosed 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] {a : α} (ha : 0 ≤ 2 • a) : 0 ≤ a - abs_abs 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : |(|a|)| = |a| - abs_nonneg 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : 0 ≤ |a| - abs_eq_zero 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a : α} [AddRightMono α] : |a| = 0 ↔ a = 0 - abs_ne_zero 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a : α} [AddRightMono α] : |a| ≠ 0 ↔ a ≠ 0 - neg_lt_of_abs_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a b : α} [AddRightMono α] (h : |a| < b) : -b < a - abs_nonpos_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a : α} [AddRightMono α] : |a| ≤ 0 ↔ a = 0 - max_sub_min_eq_abs 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] [AddRightMono α] (a b : α) : max a b - min a b = |b - a| - max_sub_min_eq_abs' 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] [AddRightMono α] (a b : α) : max a b - min a b = |a - b| - abs_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a b : α} [AddRightMono α] : |a| < b ↔ -b < a ∧ a < b - abs_le_abs_of_nonpos 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a b : α} [AddRightMono α] (ha : a ≤ 0) (hab : b ≤ a) : |a| ≤ |b| - Pi.abs_eq_zero 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{ι : Type u_2} {α : ι → Type u_3} [(i : ι) → AddGroup (α i)] (f : (i : ι) → α i) [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftMono (α i)] [∀ (i : ι), AddRightMono (α i)] : |f| = 0 ↔ f = 0 - abs_sub_lt_of_lt_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] [AddRightMono α] {N M n m : α} (hn : 0 ≤ n) (hm : 0 ≤ m) (hnN : n < N) (hmM : m < M) : |n - m| < max N M - apply_abs_le_add_of_nonneg 📋 Mathlib.Algebra.Order.Group.Abs
{G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2} [AddZeroClass H] [LE H] [AddLeftMono H] [AddRightMono H] {f : G → H} (h : ∀ (x : G), 0 ≤ f x) (a : G) : f |a| ≤ f a + f (-a) - apply_abs_le_add_of_nonneg' 📋 Mathlib.Algebra.Order.Group.Abs
{G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2} [AddZeroClass H] [LE H] [AddLeftMono H] [AddRightMono H] {f : G → H} {a : G} (h₁ : 0 ≤ f a) (h₂ : 0 ≤ f (-a)) : f |a| ≤ f a + f (-a) - WithBot.addRightMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] [LE α] [AddRightMono α] : AddRightMono (WithBot α) - WithTop.addRightMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] [LE α] [AddRightMono α] : AddRightMono (WithTop α) - WithBot.add_le_add_iff_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x y z : WithBot α} [LE α] [AddRightMono α] [AddRightReflectLE α] (hz : z ≠ ⊥) : x + z ≤ y + z ↔ x ≤ y - WithTop.add_le_add_iff_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x y z : WithTop α} [LE α] [AddRightMono α] [AddRightReflectLE α] (hz : z ≠ ⊤) : x + z ≤ y + z ↔ x ≤ y - 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 - WithBot.add_le_add_iff_right' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u_1} [Add α] [LE α] [AddRightMono α] [AddRightReflectLE α] {a b c : WithBot (WithTop α)} (hc : c ≠ ⊥) (hc' : c ≠ ⊤) : a + c ≤ b + c ↔ a ≤ b - negPart_anti 📋 Mathlib.Algebra.Order.Group.PosPart
{α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] : Antitone negPart - posPart_inf_negPart_eq_zero 📋 Mathlib.Algebra.Order.Group.PosPart
{α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : a⁺ ⊓ a⁻ = 0 - negPart_add_posPart 📋 Mathlib.Algebra.Order.Group.PosPart
{α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : a⁻ + a⁺ = |a|
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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis 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