# Ordered groups #

This file develops the basics of unbundled ordered groups.

## Implementation details #

Unfortunately, the number of `'` appended to lemmas in this file may differ between the multiplicative and the additive version of a lemma. The reason is that we did not want to change existing names in the library.

source
@[simp]
theorem Left.inv_le_one_iff {α : Type u} [Group α] [LE α] [MulLeftMono α] {a : α} :
a⁻¹ ≤ 1 ↔ 1 ≤ a

Uses `left` co(ntra)variant.

source
@[simp]
theorem Left.neg_nonpos_iff {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a : α} :
-a ≤ 0 ↔ 0 ≤ a

Uses `left` co(ntra)variant.

source
@[simp]
theorem Left.one_le_inv_iff {α : Type u} [Group α] [LE α] [MulLeftMono α] {a : α} :
1 ≤ a⁻¹ ↔ a ≤ 1

Uses `left` co(ntra)variant.

source
@[simp]
theorem Left.nonneg_neg_iff {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a : α} :
0 ≤ -a ↔ a ≤ 0

Uses `left` co(ntra)variant.

source
@[simp]
theorem le_inv_mul_iff_mul_le {α : Type u} [Group α] [LE α] [MulLeftMono α] {a b c : α} :
b ≤ a⁻¹ * c ↔ a * b ≤ c
source
@[simp]
theorem le_neg_add_iff_add_le {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b c : α} :
b ≤ -a + c ↔ a + b ≤ c
source
@[simp]
theorem inv_mul_le_iff_le_mul {α : Type u} [Group α] [LE α] [MulLeftMono α] {a b c : α} :
b⁻¹ * a ≤ c ↔ a ≤ b * c
source
@[simp]
theorem neg_add_le_iff_le_add {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b c : α} :
-b + a ≤ c ↔ a ≤ b + c
source
theorem inv_le_iff_one_le_mul' {α : Type u} [Group α] [LE α] [MulLeftMono α] {a b : α} :
a⁻¹ ≤ b ↔ 1 ≤ a * b
source
theorem neg_le_iff_add_nonneg' {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b : α} :
-a ≤ b ↔ 0 ≤ a + b
source
theorem le_inv_iff_mul_le_one_left {α : Type u} [Group α] [LE α] [MulLeftMono α] {a b : α} :
a ≤ b⁻¹ ↔ b * a ≤ 1
source
theorem le_neg_iff_add_nonpos_left {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b : α} :
a ≤ -b ↔ b + a ≤ 0
source
theorem le_inv_mul_iff_le {α : Type u} [Group α] [LE α] [MulLeftMono α] {a b : α} :
1 ≤ b⁻¹ * a ↔ b ≤ a
source
theorem le_neg_add_iff_le {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b : α} :
0 ≤ -b + a ↔ b ≤ a
source
theorem inv_mul_le_one_iff {α : Type u} [Group α] [LE α] [MulLeftMono α] {a b : α} :
a⁻¹ * b ≤ 1 ↔ b ≤ a
source
theorem neg_add_nonpos_iff {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b : α} :
-a + b ≤ 0 ↔ b ≤ a
source
@[simp]
theorem Left.one_lt_inv_iff {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a : α} :
1 < a⁻¹ ↔ a < 1

Uses `left` co(ntra)variant.

source
@[simp]
theorem Left.neg_pos_iff {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} :
0 < -a ↔ a < 0

Uses `left` co(ntra)variant.

source
@[simp]
theorem Left.inv_lt_one_iff {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a : α} :
a⁻¹ < 1 ↔ 1 < a

Uses `left` co(ntra)variant.

source
@[simp]
theorem Left.neg_neg_iff {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} :
-a < 0 ↔ 0 < a

Uses `left` co(ntra)variant.

source
@[simp]
theorem lt_inv_mul_iff_mul_lt {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b c : α} :
b < a⁻¹ * c ↔ a * b < c
source
@[simp]
theorem lt_neg_add_iff_add_lt {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
b < -a + c ↔ a + b < c
source
@[simp]
theorem inv_mul_lt_iff_lt_mul {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b c : α} :
b⁻¹ * a < c ↔ a < b * c
source
@[simp]
theorem neg_add_lt_iff_lt_add {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
-b + a < c ↔ a < b + c
source
theorem inv_lt_iff_one_lt_mul' {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b : α} :
a⁻¹ < b ↔ 1 < a * b
source
theorem neg_lt_iff_pos_add' {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} :
-a < b ↔ 0 < a + b
source
theorem lt_inv_iff_mul_lt_one' {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b : α} :
a < b⁻¹ ↔ b * a < 1
source
theorem lt_neg_iff_add_neg' {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} :
a < -b ↔ b + a < 0
source
theorem lt_inv_mul_iff_lt {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b : α} :
1 < b⁻¹ * a ↔ b < a
source
theorem lt_neg_add_iff_lt {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} :
0 < -b + a ↔ b < a
source
theorem inv_mul_lt_one_iff {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b : α} :
a⁻¹ * b < 1 ↔ b < a
source
theorem neg_add_neg_iff {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} :
-a + b < 0 ↔ b < a
source
@[simp]
theorem Right.inv_le_one_iff {α : Type u} [Group α] [LE α] [MulRightMono α] {a : α} :
a⁻¹ ≤ 1 ↔ 1 ≤ a

Uses `right` co(ntra)variant.

source
@[simp]
theorem Right.neg_nonpos_iff {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a : α} :
-a ≤ 0 ↔ 0 ≤ a

Uses `right` co(ntra)variant.

source
@[simp]
theorem Right.one_le_inv_iff {α : Type u} [Group α] [LE α] [MulRightMono α] {a : α} :
1 ≤ a⁻¹ ↔ a ≤ 1

Uses `right` co(ntra)variant.

source
@[simp]
theorem Right.nonneg_neg_iff {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a : α} :
0 ≤ -a ↔ a ≤ 0

Uses `right` co(ntra)variant.

source
theorem inv_le_iff_one_le_mul {α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} :
a⁻¹ ≤ b ↔ 1 ≤ b * a
source
theorem neg_le_iff_add_nonneg {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} :
-a ≤ b ↔ 0 ≤ b + a
source
theorem le_inv_iff_mul_le_one_right {α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} :
a ≤ b⁻¹ ↔ a * b ≤ 1
source
theorem le_neg_iff_add_nonpos_right {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} :
a ≤ -b ↔ a + b ≤ 0
source
@[simp]
theorem mul_inv_le_iff_le_mul {α : Type u} [Group α] [LE α] [MulRightMono α] {a b c : α} :
a * b⁻¹ ≤ c ↔ a ≤ c * b
source
@[simp]
theorem add_neg_le_iff_le_add {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b c : α} :
a + -b ≤ c ↔ a ≤ c + b
source
@[simp]
theorem le_mul_inv_iff_mul_le {α : Type u} [Group α] [LE α] [MulRightMono α] {a b c : α} :
c ≤ a * b⁻¹ ↔ c * b ≤ a
source
@[simp]
theorem le_add_neg_iff_add_le {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b c : α} :
c ≤ a + -b ↔ c + b ≤ a
source
theorem mul_inv_le_one_iff_le {α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} :
a * b⁻¹ ≤ 1 ↔ a ≤ b
source
theorem add_neg_nonpos_iff_le {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} :
a + -b ≤ 0 ↔ a ≤ b
source
theorem le_mul_inv_iff_le {α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} :
1 ≤ a * b⁻¹ ↔ b ≤ a
source
theorem le_add_neg_iff_le {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} :
0 ≤ a + -b ↔ b ≤ a
source
theorem mul_inv_le_one_iff {α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} :
b * a⁻¹ ≤ 1 ↔ b ≤ a
source
theorem add_neg_nonpos_iff {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} :
b + -a ≤ 0 ↔ b ≤ a
source
@[simp]
theorem Right.inv_lt_one_iff {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a : α} :
a⁻¹ < 1 ↔ 1 < a

Uses `right` co(ntra)variant.

source
@[simp]
theorem Right.neg_neg_iff {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a : α} :
-a < 0 ↔ 0 < a

Uses `right` co(ntra)variant.

source
@[simp]
theorem Right.one_lt_inv_iff {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a : α} :
1 < a⁻¹ ↔ a < 1

Uses `right` co(ntra)variant.

source
@[simp]
theorem Right.neg_pos_iff {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a : α} :
0 < -a ↔ a < 0

Uses `right` co(ntra)variant.

source
theorem inv_lt_iff_one_lt_mul {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a b : α} :
a⁻¹ < b ↔ 1 < b * a
source
theorem neg_lt_iff_pos_add {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} :
-a < b ↔ 0 < b + a
source
theorem lt_inv_iff_mul_lt_one {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a b : α} :
a < b⁻¹ ↔ a * b < 1
source
theorem lt_neg_iff_add_neg {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} :
a < -b ↔ a + b < 0
source
@[simp]
theorem mul_inv_lt_iff_lt_mul {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a b c : α} :
a * b⁻¹ < c ↔ a < c * b
source
@[simp]
theorem add_neg_lt_iff_lt_add {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} :
a + -b < c ↔ a < c + b
source
@[simp]
theorem lt_mul_inv_iff_mul_lt {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a b c : α} :
c < a * b⁻¹ ↔ c * b < a
source
@[simp]
theorem lt_add_neg_iff_add_lt {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} :
c < a + -b ↔ c + b < a
source
theorem inv_mul_lt_one_iff_lt {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a b : α} :
a * b⁻¹ < 1 ↔ a < b
source
theorem neg_add_neg_iff_lt {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} :
a + -b < 0 ↔ a < b
source
theorem lt_mul_inv_iff_lt {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a b : α} :
1 < a * b⁻¹ ↔ b < a
source
theorem lt_add_neg_iff_lt {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} :
0 < a + -b ↔ b < a
source
theorem mul_inv_lt_one_iff {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a b : α} :
b * a⁻¹ < 1 ↔ b < a
source
theorem add_neg_neg_iff {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} :
b + -a < 0 ↔ b < a
source
@[simp]
theorem div_le_self_iff {α : Type u} [Group α] [LE α] [MulLeftMono α] (a : α) {b : α} :
a / b ≤ a ↔ 1 ≤ b
source
@[simp]
theorem sub_le_self_iff {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] (a : α) {b : α} :
a - b ≤ a ↔ 0 ≤ b
source
@[simp]
theorem le_div_self_iff {α : Type u} [Group α] [LE α] [MulLeftMono α] (a : α) {b : α} :
a ≤ a / b ↔ b ≤ 1
source
@[simp]
theorem le_sub_self_iff {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] (a : α) {b : α} :
a ≤ a - b ↔ b ≤ 0
source
theorem sub_le_self {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] (a : α) {b : α} :
0 ≤ b → a - b ≤ a

Alias of the reverse direction of `sub_le_self_iff`.

source
@[simp]
theorem inv_le_inv_iff {α : Type u} [Group α] [LE α] [MulLeftMono α] {a b : α} [MulRightMono α] :
a⁻¹ ≤ b⁻¹ ↔ b ≤ a
source
@[simp]
theorem neg_le_neg_iff {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b : α} [AddRightMono α] :
-a ≤ -b ↔ b ≤ a
source
theorem le_of_neg_le_neg {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b : α} [AddRightMono α] :
-a ≤ -b → b ≤ a

Alias of the forward direction of `neg_le_neg_iff`.

source
theorem mul_inv_le_inv_mul_iff {α : Type u} [Group α] [LE α] [MulLeftMono α] {a b c d : α} [MulRightMono α] :
a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b
source
theorem add_neg_le_neg_add_iff {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b c d : α} [AddRightMono α] :
a + -b ≤ -d + c ↔ d + a ≤ c + b
source
@[simp]
theorem div_lt_self_iff {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] (a : α) {b : α} :
a / b < a ↔ 1 < b
source
@[simp]
theorem sub_lt_self_iff {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] (a : α) {b : α} :
a - b < a ↔ 0 < b
source
theorem sub_lt_self {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] (a : α) {b : α} :
0 < b → a - b < a

Alias of the reverse direction of `sub_lt_self_iff`.

source
@[simp]
theorem inv_lt_inv_iff {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b : α} [MulRightStrictMono α] :
a⁻¹ < b⁻¹ ↔ b < a
source
@[simp]
theorem neg_lt_neg_iff {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] :
-a < -b ↔ b < a
source
theorem inv_lt' {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b : α} [MulRightStrictMono α] :
a⁻¹ < b ↔ b⁻¹ < a
source
theorem neg_lt {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] :
-a < b ↔ -b < a
source
theorem lt_inv' {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b : α} [MulRightStrictMono α] :
a < b⁻¹ ↔ b < a⁻¹
source
theorem lt_neg {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] :
a < -b ↔ b < -a
source
theorem lt_inv_of_lt_inv {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b : α} [MulRightStrictMono α] :
a < b⁻¹ → b < a⁻¹

Alias of the forward direction of `lt_inv'`.

source
theorem lt_neg_of_lt_neg {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] :
a < -b → b < -a
source
theorem inv_lt_of_inv_lt' {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b : α} [MulRightStrictMono α] :
a⁻¹ < b → b⁻¹ < a

Alias of the forward direction of `inv_lt'`.

source
theorem neg_lt_of_neg_lt {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] :
-a < b → -b < a
source
theorem mul_inv_lt_inv_mul_iff {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b c d : α} [MulRightStrictMono α] :
a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b
source
theorem add_neg_lt_neg_add_iff {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c d : α} [AddRightStrictMono α] :
a + -b < -d + c ↔ d + a < c + b
source
theorem Left.inv_le_self {α : Type u} [Group α] [Preorder α] [MulLeftMono α] {a : α} (h : 1 ≤ a) :
a⁻¹ ≤ a
source
theorem Left.neg_le_self {α : Type u} [AddGroup α] [Preorder α] [AddLeftMono α] {a : α} (h : 0 ≤ a) :
-a ≤ a
source
theorem neg_le_self {α : Type u} [AddGroup α] [Preorder α] [AddLeftMono α] {a : α} (h : 0 ≤ a) :
-a ≤ a

Alias of `Left.neg_le_self`.

source
theorem Left.self_le_inv {α : Type u} [Group α] [Preorder α] [MulLeftMono α] {a : α} (h : a ≤ 1) :
a ≤ a⁻¹
source
theorem Left.self_le_neg {α : Type u} [AddGroup α] [Preorder α] [AddLeftMono α] {a : α} (h : a ≤ 0) :
a ≤ -a
source
theorem Left.inv_lt_self {α : Type u} [Group α] [Preorder α] [MulLeftStrictMono α] {a : α} (h : 1 < a) :
a⁻¹ < a
source
theorem Left.neg_lt_self {α : Type u} [AddGroup α] [Preorder α] [AddLeftStrictMono α] {a : α} (h : 0 < a) :
-a < a
source
theorem neg_lt_self {α : Type u} [AddGroup α] [Preorder α] [AddLeftStrictMono α] {a : α} (h : 0 < a) :
-a < a

Alias of `Left.neg_lt_self`.

source
theorem Left.self_lt_inv {α : Type u} [Group α] [Preorder α] [MulLeftStrictMono α] {a : α} (h : a < 1) :
a < a⁻¹
source
theorem Left.self_lt_neg {α : Type u} [AddGroup α] [Preorder α] [AddLeftStrictMono α] {a : α} (h : a < 0) :
a < -a
source
theorem Right.inv_le_self {α : Type u} [Group α] [Preorder α] [MulRightMono α] {a : α} (h : 1 ≤ a) :
a⁻¹ ≤ a
source
theorem Right.neg_le_self {α : Type u} [AddGroup α] [Preorder α] [AddRightMono α] {a : α} (h : 0 ≤ a) :
-a ≤ a
source
theorem Right.self_le_inv {α : Type u} [Group α] [Preorder α] [MulRightMono α] {a : α} (h : a ≤ 1) :
a ≤ a⁻¹
source
theorem Right.self_le_neg {α : Type u} [AddGroup α] [Preorder α] [AddRightMono α] {a : α} (h : a ≤ 0) :
a ≤ -a
source
theorem Right.inv_lt_self {α : Type u} [Group α] [Preorder α] [MulRightStrictMono α] {a : α} (h : 1 < a) :
a⁻¹ < a
source
theorem Right.neg_lt_self {α : Type u} [AddGroup α] [Preorder α] [AddRightStrictMono α] {a : α} (h : 0 < a) :
-a < a
source
theorem Right.self_lt_inv {α : Type u} [Group α] [Preorder α] [MulRightStrictMono α] {a : α} (h : a < 1) :
a < a⁻¹
source
theorem Right.self_lt_neg {α : Type u} [AddGroup α] [Preorder α] [AddRightStrictMono α] {a : α} (h : a < 0) :
a < -a
source
theorem inv_mul_le_iff_le_mul' {α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} :
c⁻¹ * a ≤ b ↔ a ≤ b * c
source
theorem neg_add_le_iff_le_add' {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c : α} :
-c + a ≤ b ↔ a ≤ b + c
source
theorem mul_inv_le_iff_le_mul' {α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} :
a * b⁻¹ ≤ c ↔ a ≤ b * c
source
theorem add_neg_le_iff_le_add' {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c : α} :
a + -b ≤ c ↔ a ≤ b + c
source
theorem mul_inv_le_mul_inv_iff' {α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c d : α} :
a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
source
theorem add_neg_le_add_neg_iff {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c d : α} :
a + -b ≤ c + -d ↔ a + d ≤ c + b
source
theorem inv_mul_lt_iff_lt_mul' {α : Type u} [CommGroup α] [LT α] [MulLeftStrictMono α] {a b c : α} :
c⁻¹ * a < b ↔ a < b * c
source
theorem neg_add_lt_iff_lt_add' {α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
-c + a < b ↔ a < b + c
source
theorem mul_inv_lt_iff_le_mul' {α : Type u} [CommGroup α] [LT α] [MulLeftStrictMono α] {a b c : α} :
a * b⁻¹ < c ↔ a < b * c
source
theorem add_neg_lt_iff_le_add' {α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
a + -b < c ↔ a < b + c
source
theorem mul_inv_lt_mul_inv_iff' {α : Type u} [CommGroup α] [LT α] [MulLeftStrictMono α] {a b c d : α} :
a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b
source
theorem add_neg_lt_add_neg_iff {α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c d : α} :
a + -b < c + -d ↔ a + d < c + b
source
theorem one_le_of_inv_le_one {α : Type u} [Group α] [LE α] [MulLeftMono α] {a : α} :
a⁻¹ ≤ 1 → 1 ≤ a

Alias of the forward direction of `Left.inv_le_one_iff`.

Uses `left` co(ntra)variant.

source
theorem nonneg_of_neg_nonpos {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a : α} :
-a ≤ 0 → 0 ≤ a
source
theorem le_one_of_one_le_inv {α : Type u} [Group α] [LE α] [MulLeftMono α] {a : α} :
1 ≤ a⁻¹ → a ≤ 1

Alias of the forward direction of `Left.one_le_inv_iff`.

Uses `left` co(ntra)variant.

source
theorem nonpos_of_neg_nonneg {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a : α} :
0 ≤ -a → a ≤ 0
source
theorem lt_of_inv_lt_inv {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b : α} [MulRightStrictMono α] :
a⁻¹ < b⁻¹ → b < a

Alias of the forward direction of `inv_lt_inv_iff`.

source
theorem lt_of_neg_lt_neg {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] :
-a < -b → b < a
source
theorem one_lt_of_inv_lt_one {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a : α} :
a⁻¹ < 1 → 1 < a

Alias of the forward direction of `Left.inv_lt_one_iff`.

Uses `left` co(ntra)variant.

source
theorem pos_of_neg_neg {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} :
-a < 0 → 0 < a
source
theorem inv_lt_one_iff_one_lt {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a : α} :
a⁻¹ < 1 ↔ 1 < a

Alias of `Left.inv_lt_one_iff`.

Uses `left` co(ntra)variant.

source
theorem neg_neg_iff_pos {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} :
-a < 0 ↔ 0 < a
source
theorem inv_lt_one' {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a : α} :
a⁻¹ < 1 ↔ 1 < a

Alias of `Left.inv_lt_one_iff`.

Uses `left` co(ntra)variant.

source
theorem neg_lt_zero {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} :
-a < 0 ↔ 0 < a
source
theorem inv_of_one_lt_inv {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a : α} :
1 < a⁻¹ → a < 1

Alias of the forward direction of `Left.one_lt_inv_iff`.

Uses `left` co(ntra)variant.

source
theorem neg_of_neg_pos {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} :
0 < -a → a < 0
source
theorem one_lt_inv_of_inv {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a : α} :
a < 1 → 1 < a⁻¹

Alias of the reverse direction of `Left.one_lt_inv_iff`.

Uses `left` co(ntra)variant.

source
theorem neg_pos_of_neg {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} :
a < 0 → 0 < -a
source
theorem mul_le_of_le_inv_mul {α : Type u} [Group α] [LE α] [MulLeftMono α] {a b c : α} :
b ≤ a⁻¹ * c → a * b ≤ c

Alias of the forward direction of `le_inv_mul_iff_mul_le`.

source
theorem add_le_of_le_neg_add {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b c : α} :
b ≤ -a + c → a + b ≤ c
source
theorem le_inv_mul_of_mul_le {α : Type u} [Group α] [LE α] [MulLeftMono α] {a b c : α} :
a * b ≤ c → b ≤ a⁻¹ * c

Alias of the reverse direction of `le_inv_mul_iff_mul_le`.

source
theorem le_neg_add_of_add_le {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b c : α} :
a + b ≤ c → b ≤ -a + c
source
theorem inv_mul_le_of_le_mul {α : Type u} [Group α] [LE α] [MulLeftMono α] {a b c : α} :
a ≤ b * c → b⁻¹ * a ≤ c

Alias of the reverse direction of `inv_mul_le_iff_le_mul`.

source
theorem neg_add_le_of_le_add {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a b c : α} :
a ≤ b + c → -b + a ≤ c
source
theorem mul_lt_of_lt_inv_mul {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b c : α} :
b < a⁻¹ * c → a * b < c

Alias of the forward direction of `lt_inv_mul_iff_mul_lt`.

source
theorem add_lt_of_lt_neg_add {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
b < -a + c → a + b < c
source
theorem lt_inv_mul_of_mul_lt {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b c : α} :
a * b < c → b < a⁻¹ * c

Alias of the reverse direction of `lt_inv_mul_iff_mul_lt`.

source
theorem lt_neg_add_of_add_lt {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
a + b < c → b < -a + c
source
theorem inv_mul_lt_of_lt_mul {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b c : α} :
a < b * c → b⁻¹ * a < c

Alias of the reverse direction of `inv_mul_lt_iff_lt_mul`.

source
theorem lt_mul_of_inv_mul_lt {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b c : α} :
b⁻¹ * a < c → a < b * c

Alias of the forward direction of `inv_mul_lt_iff_lt_mul`.

source
theorem lt_add_of_neg_add_lt {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
-b + a < c → a < b + c
source
theorem neg_add_lt_of_lt_add {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
a < b + c → -b + a < c
source
theorem lt_mul_of_inv_mul_lt_left {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a b c : α} :
b⁻¹ * a < c → a < b * c

Alias of the forward direction of `inv_mul_lt_iff_lt_mul`.

Alias of the forward direction of `inv_mul_lt_iff_lt_mul`.

source
theorem lt_add_of_neg_add_lt_left {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
-b + a < c → a < b + c
source
theorem inv_le_one' {α : Type u} [Group α] [LE α] [MulLeftMono α] {a : α} :
a⁻¹ ≤ 1 ↔ 1 ≤ a

Alias of `Left.inv_le_one_iff`.

Uses `left` co(ntra)variant.

source
theorem neg_nonpos {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a : α} :
-a ≤ 0 ↔ 0 ≤ a
source
theorem one_le_inv' {α : Type u} [Group α] [LE α] [MulLeftMono α] {a : α} :
1 ≤ a⁻¹ ↔ a ≤ 1

Alias of `Left.one_le_inv_iff`.

Uses `left` co(ntra)variant.

source
theorem neg_nonneg {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a : α} :
0 ≤ -a ↔ a ≤ 0
source
theorem one_lt_inv' {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] {a : α} :
1 < a⁻¹ ↔ a < 1

Alias of `Left.one_lt_inv_iff`.

Uses `left` co(ntra)variant.

source
theorem neg_pos {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a : α} :
0 < -a ↔ a < 0
source
theorem div_le_div_iff_right {α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} (c : α) :
a / c ≤ b / c ↔ a ≤ b
source
theorem sub_le_sub_iff_right {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} (c : α) :
a - c ≤ b - c ↔ a ≤ b
source
theorem div_le_div_right' {α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} (h : a ≤ b) (c : α) :
a / c ≤ b / c
source
theorem sub_le_sub_right {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} (h : a ≤ b) (c : α) :
a - c ≤ b - c
source
@[simp]
theorem one_le_div' {α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} :
1 ≤ a / b ↔ b ≤ a
source
@[simp]
theorem sub_nonneg {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} :
0 ≤ a - b ↔ b ≤ a
source
theorem le_of_sub_nonneg {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} :
0 ≤ a - b → b ≤ a

Alias of the forward direction of `sub_nonneg`.

source
theorem sub_nonneg_of_le {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} :
b ≤ a → 0 ≤ a - b

Alias of the reverse direction of `sub_nonneg`.

source
theorem div_le_one' {α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} :
a / b ≤ 1 ↔ a ≤ b
source
theorem sub_nonpos {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} :
a - b ≤ 0 ↔ a ≤ b
source
theorem sub_nonpos_of_le {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} :
a ≤ b → a - b ≤ 0

Alias of the reverse direction of `sub_nonpos`.

source
theorem le_of_sub_nonpos {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b : α} :
a - b ≤ 0 → a ≤ b

Alias of the forward direction of `sub_nonpos`.

source
theorem le_div_iff_mul_le {α : Type u} [Group α] [LE α] [MulRightMono α] {a b c : α} :
a ≤ c / b ↔ a * b ≤ c
source
theorem le_sub_iff_add_le {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b c : α} :
a ≤ c - b ↔ a + b ≤ c
source
theorem add_le_of_le_sub_right {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b c : α} :
a ≤ c - b → a + b ≤ c

Alias of the forward direction of `le_sub_iff_add_le`.

source
theorem le_sub_right_of_add_le {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b c : α} :
a + b ≤ c → a ≤ c - b

Alias of the reverse direction of `le_sub_iff_add_le`.

source
@[simp]
theorem div_le_iff_le_mul {α : Type u} [Group α] [LE α] [MulRightMono α] {a b c : α} :
a / c ≤ b ↔ a ≤ b * c
source
theorem sub_le_iff_le_add {α : Type u} [AddGroup α] [LE α] [AddRightMono α] {a b c : α} :
a - c ≤ b ↔ a ≤ b + c
source
@[instance 100]
instance AddGroup.toOrderedSub {α : Type u_1} [AddGroup α] [LE α] [AddRightMono α] :
OrderedSub α
source
theorem div_le_div_iff_left {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] {b c : α} (a : α) :
a / b ≤ a / c ↔ c ≤ b
source
theorem sub_le_sub_iff_left {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {b c : α} (a : α) :
a - b ≤ a - c ↔ c ≤ b
source
theorem div_le_div_left' {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] {a b : α} (h : a ≤ b) (c : α) :
c / b ≤ c / a
source
theorem sub_le_sub_left {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {a b : α} (h : a ≤ b) (c : α) :
c - b ≤ c - a
source
theorem div_le_div_iff' {α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c d : α} :
a / b ≤ c / d ↔ a * d ≤ c * b

See also `div_le_div_iff` for a version that works for `LinearOrderedSemifield` with additional assumptions.

source
theorem sub_le_sub_iff {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c d : α} :
a - b ≤ c - d ↔ a + d ≤ c + b
source
theorem le_div_iff_mul_le' {α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} :
b ≤ c / a ↔ a * b ≤ c
source
theorem le_sub_iff_add_le' {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c : α} :
b ≤ c - a ↔ a + b ≤ c
source
theorem le_sub_left_of_add_le {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c : α} :
a + b ≤ c → b ≤ c - a

Alias of the reverse direction of `le_sub_iff_add_le'`.

source
theorem add_le_of_le_sub_left {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c : α} :
b ≤ c - a → a + b ≤ c

Alias of the forward direction of `le_sub_iff_add_le'`.

source
theorem div_le_iff_le_mul' {α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} :
a / b ≤ c ↔ a ≤ b * c
source
theorem sub_le_iff_le_add' {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c : α} :
a - b ≤ c ↔ a ≤ b + c
source
theorem le_add_of_sub_left_le {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c : α} :
a - b ≤ c → a ≤ b + c

Alias of the forward direction of `sub_le_iff_le_add'`.

source
theorem sub_left_le_of_le_add {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c : α} :
a ≤ b + c → a - b ≤ c

Alias of the reverse direction of `sub_le_iff_le_add'`.

source
@[simp]
theorem inv_le_div_iff_le_mul {α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} :
b⁻¹ ≤ a / c ↔ c ≤ a * b
source
@[simp]
theorem neg_le_sub_iff_le_add {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c : α} :
-b ≤ a - c ↔ c ≤ a + b
source
theorem inv_le_div_iff_le_mul' {α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} :
a⁻¹ ≤ b / c ↔ c ≤ a * b
source
theorem neg_le_sub_iff_le_add' {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c : α} :
-a ≤ b - c ↔ c ≤ a + b
source
theorem div_le_comm {α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} :
a / b ≤ c ↔ a / c ≤ b
source
theorem sub_le_comm {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c : α} :
a - b ≤ c ↔ a - c ≤ b
source
theorem le_div_comm {α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} :
a ≤ b / c ↔ c ≤ b / a
source
theorem le_sub_comm {α : Type u} [AddCommGroup α] [LE α] [AddLeftMono α] {a b c : α} :
a ≤ b - c ↔ c ≤ b - a
source
theorem div_le_div'' {α : Type u} [CommGroup α] [Preorder α] [MulLeftMono α] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) :
a / d ≤ b / c
source
theorem sub_le_sub {α : Type u} [AddCommGroup α] [Preorder α] [AddLeftMono α] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) :
a - d ≤ b - c
source
@[simp]
theorem div_lt_div_iff_right {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a b : α} (c : α) :
a / c < b / c ↔ a < b
source
@[simp]
theorem sub_lt_sub_iff_right {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} (c : α) :
a - c < b - c ↔ a < b
source
theorem div_lt_div_right' {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a b : α} (h : a < b) (c : α) :
a / c < b / c
source
theorem sub_lt_sub_right {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} (h : a < b) (c : α) :
a - c < b - c
source
@[simp]
theorem one_lt_div' {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a b : α} :
1 < a / b ↔ b < a
source
@[simp]
theorem sub_pos {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} :
0 < a - b ↔ b < a
source
theorem lt_of_sub_pos {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} :
0 < a - b → b < a

Alias of the forward direction of `sub_pos`.

source
theorem sub_pos_of_lt {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} :
b < a → 0 < a - b

Alias of the reverse direction of `sub_pos`.

source
@[simp]
theorem div_lt_one' {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a b : α} :
a / b < 1 ↔ a < b
source
@[simp]
theorem sub_neg {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} :
a - b < 0 ↔ a < b

For `a - -b = a + b`, see `sub_neg_eq_add`.

source
theorem sub_neg_of_lt {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} :
a < b → a - b < 0

Alias of the reverse direction of `sub_neg`.

For `a - -b = a + b`, see `sub_neg_eq_add`.

source
theorem lt_of_sub_neg {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} :
a - b < 0 → a < b

Alias of the forward direction of `sub_neg`.

For `a - -b = a + b`, see `sub_neg_eq_add`.

source
theorem sub_lt_zero {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} :
a - b < 0 ↔ a < b

Alias of `sub_neg`.

For `a - -b = a + b`, see `sub_neg_eq_add`.

source
theorem lt_div_iff_mul_lt {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a b c : α} :
a < c / b ↔ a * b < c
source
theorem lt_sub_iff_add_lt {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} :
a < c - b ↔ a + b < c
source
theorem add_lt_of_lt_sub_right {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} :
a < c - b → a + b < c

Alias of the forward direction of `lt_sub_iff_add_lt`.

source
theorem lt_sub_right_of_add_lt {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} :
a + b < c → a < c - b

Alias of the reverse direction of `lt_sub_iff_add_lt`.

source
theorem div_lt_iff_lt_mul {α : Type u} [Group α] [LT α] [MulRightStrictMono α] {a b c : α} :
a / c < b ↔ a < b * c
source
theorem sub_lt_iff_lt_add {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} :
a - c < b ↔ a < b + c
source
theorem lt_add_of_sub_right_lt {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} :
a - c < b → a < b + c

Alias of the forward direction of `sub_lt_iff_lt_add`.

source
theorem sub_right_lt_of_lt_add {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} :
a < b + c → a - c < b

Alias of the reverse direction of `sub_lt_iff_lt_add`.

source
@[simp]
theorem div_lt_div_iff_left {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] [MulRightStrictMono α] {b c : α} (a : α) :
a / b < a / c ↔ c < b
source
@[simp]
theorem sub_lt_sub_iff_left {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] [AddRightStrictMono α] {b c : α} (a : α) :
a - b < a - c ↔ c < b
source
@[simp]
theorem inv_lt_div_iff_lt_mul {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] [MulRightStrictMono α] {a b c : α} :
a⁻¹ < b / c ↔ c < a * b
source
@[simp]
theorem neg_lt_sub_iff_lt_add {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] [AddRightStrictMono α] {a b c : α} :
-a < b - c ↔ c < a + b
source
theorem div_lt_div_left' {α : Type u} [Group α] [LT α] [MulLeftStrictMono α] [MulRightStrictMono α] {a b : α} (h : a < b) (c : α) :
c / b < c / a
source
theorem sub_lt_sub_left {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] [AddRightStrictMono α] {a b : α} (h : a < b) (c : α) :
c - b < c - a
source
theorem div_lt_div_iff' {α : Type u} [CommGroup α] [LT α] [MulLeftStrictMono α] {a b c d : α} :
a / b < c / d ↔ a * d < c * b
source
theorem sub_lt_sub_iff {α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c d : α} :
a - b < c - d ↔ a + d < c + b
source
theorem lt_div_iff_mul_lt' {α : Type u} [CommGroup α] [LT α] [MulLeftStrictMono α] {a b c : α} :
b < c / a ↔ a * b < c
source
theorem lt_sub_iff_add_lt' {α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
b < c - a ↔ a + b < c
source
theorem lt_sub_left_of_add_lt {α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
a + b < c → b < c - a

Alias of the reverse direction of `lt_sub_iff_add_lt'`.

source
theorem add_lt_of_lt_sub_left {α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
b < c - a → a + b < c

Alias of the forward direction of `lt_sub_iff_add_lt'`.

source
theorem div_lt_iff_lt_mul' {α : Type u} [CommGroup α] [LT α] [MulLeftStrictMono α] {a b c : α} :
a / b < c ↔ a < b * c
source
theorem sub_lt_iff_lt_add' {α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
a - b < c ↔ a < b + c
source
theorem sub_left_lt_of_lt_add {α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
a < b + c → a - b < c

Alias of the reverse direction of `sub_lt_iff_lt_add'`.

source
theorem lt_add_of_sub_left_lt {α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
a - b < c → a < b + c

Alias of the forward direction of `sub_lt_iff_lt_add'`.

source
theorem inv_lt_div_iff_lt_mul' {α : Type u} [CommGroup α] [LT α] [MulLeftStrictMono α] {a b c : α} :
b⁻¹ < a / c ↔ c < a * b
source
theorem neg_lt_sub_iff_lt_add' {α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
-b < a - c ↔ c < a + b
source
theorem div_lt_comm {α : Type u} [CommGroup α] [LT α] [MulLeftStrictMono α] {a b c : α} :
a / b < c ↔ a / c < b
source
theorem sub_lt_comm {α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
a - b < c ↔ a - c < b
source
theorem lt_div_comm {α : Type u} [CommGroup α] [LT α] [MulLeftStrictMono α] {a b c : α} :
a < b / c ↔ c < b / a
source
theorem lt_sub_comm {α : Type u} [AddCommGroup α] [LT α] [AddLeftStrictMono α] {a b c : α} :
a < b - c ↔ c < b - a
source
theorem div_lt_div'' {α : Type u} [CommGroup α] [Preorder α] [MulLeftStrictMono α] {a b c d : α} (hab : a < b) (hcd : c < d) :
a / d < b / c
source
theorem sub_lt_sub {α : Type u} [AddCommGroup α] [Preorder α] [AddLeftStrictMono α] {a b c d : α} (hab : a < b) (hcd : c < d) :
a - d < b - c
source
theorem lt_or_lt_of_div_lt_div {α : Type u} [CommGroup α] [LinearOrder α] [MulLeftMono α] {a b c d : α} :
a / d < b / c → a < b ∨ c < d
source
theorem lt_or_lt_of_sub_lt_sub {α : Type u} [AddCommGroup α] [LinearOrder α] [AddLeftMono α] {a b c d : α} :
a - d < b - c → a < b ∨ c < d
source
@[simp]
theorem cmp_div_one' {α : Type u} [Group α] [LinearOrder α] [MulRightMono α] (a b : α) :
cmp (a / b) 1 = cmp a b
source
@[simp]
theorem cmp_sub_zero {α : Type u} [AddGroup α] [LinearOrder α] [AddRightMono α] (a b : α) :
cmp (a - b) 0 = cmp a b
source
theorem le_of_forall_one_lt_lt_mul {α : Type u} [Group α] [LinearOrder α] [MulLeftMono α] {a b : α} (h : ∀ (ε : α), 1 < ε → a < b * ε) :
a ≤ b
source
theorem le_of_forall_pos_lt_add {α : Type u} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a b : α} (h : ∀ (ε : α), 0 < ε → a < b + ε) :
a ≤ b
source
theorem le_iff_forall_one_lt_lt_mul {α : Type u} [Group α] [LinearOrder α] [MulLeftMono α] {a b : α} :
a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε
source
theorem le_iff_forall_pos_lt_add {α : Type u} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a b : α} :
a ≤ b ↔ ∀ (ε : α), 0 < ε → a < b + ε
source
theorem div_le_inv_mul_iff {α : Type u} [Group α] [LinearOrder α] [MulLeftMono α] {a b : α} [MulRightMono α] :
a / b ≤ a⁻¹ * b ↔ a ≤ b
source
theorem sub_le_neg_add_iff {α : Type u} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a b : α} [AddRightMono α] :
a - b ≤ -a + b ↔ a ≤ b
source
theorem div_le_div_flip {α : Type u_1} [CommGroup α] [LinearOrder α] [MulLeftMono α] {a b : α} :
a / b ≤ b / a ↔ a ≤ b
source
theorem sub_le_sub_flip {α : Type u_1} [AddCommGroup α] [LinearOrder α] [AddLeftMono α] {a b : α} :
a - b ≤ b - a ↔ a ≤ b
source
theorem Monotone.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftMono α] [MulRightMono α] [Preorder β] {f : β → α} (hf : Monotone f) :
Antitone fun (x : β) => (f x)⁻¹
source
theorem Monotone.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftMono α] [AddRightMono α] [Preorder β] {f : β → α} (hf : Monotone f) :
Antitone fun (x : β) => -f x
source
theorem Antitone.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftMono α] [MulRightMono α] [Preorder β] {f : β → α} (hf : Antitone f) :
Monotone fun (x : β) => (f x)⁻¹
source
theorem Antitone.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftMono α] [AddRightMono α] [Preorder β] {f : β → α} (hf : Antitone f) :
Monotone fun (x : β) => -f x
source
theorem MonotoneOn.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftMono α] [MulRightMono α] [Preorder β] {f : β → α} {s : Set β} (hf : MonotoneOn f s) :
AntitoneOn (fun (x : β) => (f x)⁻¹) s
source
theorem MonotoneOn.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftMono α] [AddRightMono α] [Preorder β] {f : β → α} {s : Set β} (hf : MonotoneOn f s) :
AntitoneOn (fun (x : β) => -f x) s
source
theorem AntitoneOn.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftMono α] [MulRightMono α] [Preorder β] {f : β → α} {s : Set β} (hf : AntitoneOn f s) :
MonotoneOn (fun (x : β) => (f x)⁻¹) s
source
theorem AntitoneOn.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftMono α] [AddRightMono α] [Preorder β] {f : β → α} {s : Set β} (hf : AntitoneOn f s) :
MonotoneOn (fun (x : β) => -f x) s
source
theorem StrictMono.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftStrictMono α] [MulRightStrictMono α] [Preorder β] {f : β → α} (hf : StrictMono f) :
StrictAnti fun (x : β) => (f x)⁻¹
source
theorem StrictMono.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} (hf : StrictMono f) :
StrictAnti fun (x : β) => -f x
source
theorem StrictAnti.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftStrictMono α] [MulRightStrictMono α] [Preorder β] {f : β → α} (hf : StrictAnti f) :
StrictMono fun (x : β) => (f x)⁻¹
source
theorem StrictAnti.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} (hf : StrictAnti f) :
StrictMono fun (x : β) => -f x
source
theorem StrictMonoOn.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftStrictMono α] [MulRightStrictMono α] [Preorder β] {f : β → α} {s : Set β} (hf : StrictMonoOn f s) :
StrictAntiOn (fun (x : β) => (f x)⁻¹) s
source
theorem StrictMonoOn.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} {s : Set β} (hf : StrictMonoOn f s) :
StrictAntiOn (fun (x : β) => -f x) s
source
theorem StrictAntiOn.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftStrictMono α] [MulRightStrictMono α] [Preorder β] {f : β → α} {s : Set β} (hf : StrictAntiOn f s) :
StrictMonoOn (fun (x : β) => (f x)⁻¹) s
source
theorem StrictAntiOn.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} {s : Set β} (hf : StrictAntiOn f s) :
StrictMonoOn (fun (x : β) => -f x) s