Documentation

Mathlib.Algebra.Order.Group.Unbundled.Basic

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.

@[simp]
theorem Left.neg_nonpos_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} :
-a 0 0 a

Uses left co(ntra)variant.

@[simp]
theorem Left.inv_le_one_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} :
a⁻¹ 1 1 a

Uses left co(ntra)variant.

@[simp]
theorem Left.nonneg_neg_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} :
0 -a a 0

Uses left co(ntra)variant.

@[simp]
theorem Left.one_le_inv_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} :
1 a⁻¹ a 1

Uses left co(ntra)variant.

@[simp]
theorem le_neg_add_iff_add_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
b -a + c a + b c
@[simp]
theorem le_inv_mul_iff_mul_le {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
b a⁻¹ * c a * b c
@[simp]
theorem neg_add_le_iff_le_add {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
-b + a c a b + c
@[simp]
theorem inv_mul_le_iff_le_mul {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
b⁻¹ * a c a b * c
theorem neg_le_iff_add_nonneg' {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
-a b 0 a + b
theorem inv_le_iff_one_le_mul' {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
a⁻¹ b 1 a * b
theorem le_neg_iff_add_nonpos_left {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
a -b b + a 0
theorem le_inv_iff_mul_le_one_left {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
a b⁻¹ b * a 1
theorem le_neg_add_iff_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
0 -b + a b a
theorem le_inv_mul_iff_le {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
1 b⁻¹ * a b a
theorem neg_add_nonpos_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
-a + b 0 b a
theorem inv_mul_le_one_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
a⁻¹ * b 1 b a
@[simp]
theorem Left.neg_pos_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
0 < -a a < 0

Uses left co(ntra)variant.

@[simp]
theorem Left.one_lt_inv_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
1 < a⁻¹ a < 1

Uses left co(ntra)variant.

@[simp]
theorem Left.neg_neg_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
-a < 0 0 < a

Uses left co(ntra)variant.

@[simp]
theorem Left.inv_lt_one_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
a⁻¹ < 1 1 < a

Uses left co(ntra)variant.

@[simp]
theorem lt_neg_add_iff_add_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
b < -a + c a + b < c
@[simp]
theorem lt_inv_mul_iff_mul_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
b < a⁻¹ * c a * b < c
@[simp]
theorem neg_add_lt_iff_lt_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
-b + a < c a < b + c
@[simp]
theorem inv_mul_lt_iff_lt_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
b⁻¹ * a < c a < b * c
theorem neg_lt_iff_pos_add' {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
-a < b 0 < a + b
theorem inv_lt_iff_one_lt_mul' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a⁻¹ < b 1 < a * b
theorem lt_neg_iff_add_neg' {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a < -b b + a < 0
theorem lt_inv_iff_mul_lt_one' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a < b⁻¹ b * a < 1
theorem lt_neg_add_iff_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
0 < -b + a b < a
theorem lt_inv_mul_iff_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
1 < b⁻¹ * a b < a
theorem neg_add_neg_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
-a + b < 0 b < a
theorem inv_mul_lt_one_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a⁻¹ * b < 1 b < a
@[simp]
theorem Right.neg_nonpos_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} :
-a 0 0 a

Uses right co(ntra)variant.

@[simp]
theorem Right.inv_le_one_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} :
a⁻¹ 1 1 a

Uses right co(ntra)variant.

@[simp]
theorem Right.nonneg_neg_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} :
0 -a a 0

Uses right co(ntra)variant.

@[simp]
theorem Right.one_le_inv_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} :
1 a⁻¹ a 1

Uses right co(ntra)variant.

theorem neg_le_iff_add_nonneg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
-a b 0 b + a
theorem inv_le_iff_one_le_mul {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
a⁻¹ b 1 b * a
theorem le_neg_iff_add_nonpos_right {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
a -b a + b 0
theorem le_inv_iff_mul_le_one_right {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
a b⁻¹ a * b 1
@[simp]
theorem add_neg_le_iff_le_add {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a + -b c a c + b
@[simp]
theorem mul_inv_le_iff_le_mul {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a * b⁻¹ c a c * b
@[simp]
theorem le_add_neg_iff_add_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
c a + -b c + b a
@[simp]
theorem le_mul_inv_iff_mul_le {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
c a * b⁻¹ c * b a
theorem add_neg_nonpos_iff_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
a + -b 0 a b
theorem mul_inv_le_one_iff_le {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
a * b⁻¹ 1 a b
theorem le_add_neg_iff_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
0 a + -b b a
theorem le_mul_inv_iff_le {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
1 a * b⁻¹ b a
theorem add_neg_nonpos_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
b + -a 0 b a
theorem mul_inv_le_one_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
b * a⁻¹ 1 b a
@[simp]
theorem Right.neg_neg_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
-a < 0 0 < a

Uses right co(ntra)variant.

@[simp]
theorem Right.inv_lt_one_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
a⁻¹ < 1 1 < a

Uses right co(ntra)variant.

@[simp]
theorem Right.neg_pos_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
0 < -a a < 0

Uses right co(ntra)variant.

@[simp]
theorem Right.one_lt_inv_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
1 < a⁻¹ a < 1

Uses right co(ntra)variant.

theorem neg_lt_iff_pos_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
-a < b 0 < b + a
theorem inv_lt_iff_one_lt_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a⁻¹ < b 1 < b * a
theorem lt_neg_iff_add_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a < -b a + b < 0
theorem lt_inv_iff_mul_lt_one {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a < b⁻¹ a * b < 1
@[simp]
theorem add_neg_lt_iff_lt_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a + -b < c a < c + b
@[simp]
theorem mul_inv_lt_iff_lt_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a * b⁻¹ < c a < c * b
@[simp]
theorem lt_add_neg_iff_add_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
c < a + -b c + b < a
@[simp]
theorem lt_mul_inv_iff_mul_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
c < a * b⁻¹ c * b < a
theorem neg_add_neg_iff_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a + -b < 0 a < b
theorem inv_mul_lt_one_iff_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a * b⁻¹ < 1 a < b
theorem lt_add_neg_iff_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
0 < a + -b b < a
theorem lt_mul_inv_iff_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
1 < a * b⁻¹ b < a
theorem add_neg_neg_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
b + -a < 0 b < a
theorem mul_inv_lt_one_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
b * a⁻¹ < 1 b < a
@[simp]
theorem sub_le_self_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) {b : α} :
a - b a 0 b
@[simp]
theorem div_le_self_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) {b : α} :
a / b a 1 b
@[simp]
theorem le_sub_self_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) {b : α} :
a a - b b 0
@[simp]
theorem le_div_self_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) {b : α} :
a a / b b 1
theorem sub_le_self {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) {b : α} :
0 ba - b a

Alias of the reverse direction of sub_le_self_iff.

@[simp]
theorem neg_le_neg_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
-a -b b a
@[simp]
theorem inv_le_inv_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
theorem le_of_neg_le_neg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
-a -bb a

Alias of the forward direction of neg_le_neg_iff.

theorem add_neg_le_neg_add_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} {d : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
a + -b -d + c d + a c + b
theorem mul_inv_le_inv_mul_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} {d : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
a * b⁻¹ d⁻¹ * c d * a c * b
@[simp]
theorem sub_lt_self_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (a : α) {b : α} :
a - b < a 0 < b
@[simp]
theorem div_lt_self_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] (a : α) {b : α} :
a / b < a 1 < b
theorem sub_lt_self {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (a : α) {b : α} :
0 < ba - b < a

Alias of the reverse direction of sub_lt_self_iff.

@[simp]
theorem neg_lt_neg_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] :
-a < -b b < a
@[simp]
theorem inv_lt_inv_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] :
a⁻¹ < b⁻¹ b < a
theorem neg_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] :
-a < b -b < a
theorem inv_lt' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] :
a⁻¹ < b b⁻¹ < a
theorem lt_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] :
a < -b b < -a
theorem lt_inv' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] :
a < b⁻¹ b < a⁻¹
theorem lt_inv_of_lt_inv {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] :
a < b⁻¹b < a⁻¹

Alias of the forward direction of lt_inv'.

theorem lt_neg_of_lt_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] :
a < -bb < -a
theorem inv_lt_of_inv_lt' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] :
a⁻¹ < bb⁻¹ < a

Alias of the forward direction of inv_lt'.

theorem neg_lt_of_neg_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] :
-a < b-b < a
theorem add_neg_lt_neg_add_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] :
a + -b < -d + c d + a < c + b
theorem mul_inv_lt_inv_mul_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] :
a * b⁻¹ < d⁻¹ * c d * a < c * b
theorem Left.neg_le_self {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} (h : 0 a) :
-a a
theorem Left.inv_le_self {α : Type u} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} (h : 1 a) :
theorem neg_le_self {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} (h : 0 a) :
-a a

Alias of Left.neg_le_self.

theorem Left.self_le_neg {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} (h : a 0) :
a -a
theorem Left.self_le_inv {α : Type u} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} (h : a 1) :
theorem Left.neg_lt_self {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : 0 < a) :
-a < a
theorem Left.inv_lt_self {α : Type u} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : 1 < a) :
a⁻¹ < a
theorem neg_lt_self {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : 0 < a) :
-a < a

Alias of Left.neg_lt_self.

theorem Left.self_lt_neg {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : a < 0) :
a < -a
theorem Left.self_lt_inv {α : Type u} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : a < 1) :
a < a⁻¹
theorem Right.neg_le_self {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} (h : 0 a) :
-a a
theorem Right.inv_le_self {α : Type u} [Group α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} (h : 1 a) :
theorem Right.self_le_neg {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} (h : a 0) :
a -a
theorem Right.self_le_inv {α : Type u} [Group α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} (h : a 1) :
theorem Right.neg_lt_self {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : 0 < a) :
-a < a
theorem Right.inv_lt_self {α : Type u} [Group α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : 1 < a) :
a⁻¹ < a
theorem Right.self_lt_neg {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : a < 0) :
a < -a
theorem Right.self_lt_inv {α : Type u} [Group α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : a < 1) :
a < a⁻¹
theorem neg_add_le_iff_le_add' {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
-c + a b a b + c
theorem inv_mul_le_iff_le_mul' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
c⁻¹ * a b a b * c
theorem add_neg_le_iff_le_add' {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a + -b c a b + c
theorem mul_inv_le_iff_le_mul' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a * b⁻¹ c a b * c
theorem add_neg_le_add_neg_iff {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} {d : α} :
a + -b c + -d a + d c + b
theorem mul_inv_le_mul_inv_iff' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} {d : α} :
a * b⁻¹ c * d⁻¹ a * d c * b
theorem neg_add_lt_iff_lt_add' {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
-c + a < b a < b + c
theorem inv_mul_lt_iff_lt_mul' {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
c⁻¹ * a < b a < b * c
theorem add_neg_lt_iff_le_add' {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a + -b < c a < b + c
theorem mul_inv_lt_iff_le_mul' {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a * b⁻¹ < c a < b * c
theorem add_neg_lt_add_neg_iff {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} :
a + -b < c + -d a + d < c + b
theorem mul_inv_lt_mul_inv_iff' {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} :
a * b⁻¹ < c * d⁻¹ a * d < c * b
theorem one_le_of_inv_le_one {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} :
a⁻¹ 11 a

Alias of the forward direction of Left.inv_le_one_iff.


Uses left co(ntra)variant.

theorem nonneg_of_neg_nonpos {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} :
-a 00 a
theorem le_one_of_one_le_inv {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} :
1 a⁻¹a 1

Alias of the forward direction of Left.one_le_inv_iff.


Uses left co(ntra)variant.

theorem nonpos_of_neg_nonneg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} :
0 -aa 0
theorem lt_of_inv_lt_inv {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] :
a⁻¹ < b⁻¹b < a

Alias of the forward direction of inv_lt_inv_iff.

theorem lt_of_neg_lt_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] :
-a < -bb < a
theorem one_lt_of_inv_lt_one {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
a⁻¹ < 11 < a

Alias of the forward direction of Left.inv_lt_one_iff.


Uses left co(ntra)variant.

theorem pos_of_neg_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
-a < 00 < a
theorem inv_lt_one_iff_one_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
a⁻¹ < 1 1 < a

Alias of Left.inv_lt_one_iff.


Uses left co(ntra)variant.

theorem neg_neg_iff_pos {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
-a < 0 0 < a
theorem inv_lt_one' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
a⁻¹ < 1 1 < a

Alias of Left.inv_lt_one_iff.


Uses left co(ntra)variant.

theorem neg_lt_zero {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
-a < 0 0 < a
theorem inv_of_one_lt_inv {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
1 < a⁻¹a < 1

Alias of the forward direction of Left.one_lt_inv_iff.


Uses left co(ntra)variant.

theorem neg_of_neg_pos {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
0 < -aa < 0
theorem one_lt_inv_of_inv {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
a < 11 < a⁻¹

Alias of the reverse direction of Left.one_lt_inv_iff.


Uses left co(ntra)variant.

theorem neg_pos_of_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
a < 00 < -a
theorem mul_le_of_le_inv_mul {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
b a⁻¹ * ca * b c

Alias of the forward direction of le_inv_mul_iff_mul_le.

theorem add_le_of_le_neg_add {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
b -a + ca + b c
theorem le_inv_mul_of_mul_le {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a * b cb a⁻¹ * c

Alias of the reverse direction of le_inv_mul_iff_mul_le.

theorem le_neg_add_of_add_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a + b cb -a + c
theorem inv_mul_le_of_le_mul {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a b * cb⁻¹ * a c

Alias of the reverse direction of inv_mul_le_iff_le_mul.

theorem neg_add_le_of_le_add {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a b + c-b + a c
theorem mul_lt_of_lt_inv_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
b < a⁻¹ * ca * b < c

Alias of the forward direction of lt_inv_mul_iff_mul_lt.

theorem add_lt_of_lt_neg_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
b < -a + ca + b < c
theorem lt_inv_mul_of_mul_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a * b < cb < a⁻¹ * c

Alias of the reverse direction of lt_inv_mul_iff_mul_lt.

theorem lt_neg_add_of_add_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a + b < cb < -a + c
theorem lt_mul_of_inv_mul_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
b⁻¹ * a < ca < b * c

Alias of the forward direction of inv_mul_lt_iff_lt_mul.

theorem inv_mul_lt_of_lt_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a < b * cb⁻¹ * a < c

Alias of the reverse direction of inv_mul_lt_iff_lt_mul.

theorem lt_add_of_neg_add_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
-b + a < ca < b + c
theorem neg_add_lt_of_lt_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a < b + c-b + a < c
theorem lt_mul_of_inv_mul_lt_left {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
b⁻¹ * a < ca < 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.

theorem lt_add_of_neg_add_lt_left {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
-b + a < ca < b + c
theorem inv_le_one' {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} :
a⁻¹ 1 1 a

Alias of Left.inv_le_one_iff.


Uses left co(ntra)variant.

theorem neg_nonpos {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} :
-a 0 0 a
theorem one_le_inv' {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} :
1 a⁻¹ a 1

Alias of Left.one_le_inv_iff.


Uses left co(ntra)variant.

theorem neg_nonneg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} :
0 -a a 0
theorem one_lt_inv' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
1 < a⁻¹ a < 1

Alias of Left.one_lt_inv_iff.


Uses left co(ntra)variant.

theorem neg_pos {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} :
0 < -a a < 0
theorem sub_le_sub_iff_right {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} (c : α) :
a - c b - c a b
theorem div_le_div_iff_right {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} (c : α) :
a / c b / c a b
theorem sub_le_sub_right {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} (h : a b) (c : α) :
a - c b - c
theorem div_le_div_right' {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} (h : a b) (c : α) :
a / c b / c
@[simp]
theorem sub_nonneg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
0 a - b b a
@[simp]
theorem one_le_div' {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
1 a / b b a
theorem le_of_sub_nonneg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
0 a - bb a

Alias of the forward direction of sub_nonneg.

theorem sub_nonneg_of_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
b a0 a - b

Alias of the reverse direction of sub_nonneg.

theorem sub_nonpos {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
a - b 0 a b
theorem div_le_one' {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
a / b 1 a b
theorem le_of_sub_nonpos {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
a - b 0a b

Alias of the forward direction of sub_nonpos.

theorem sub_nonpos_of_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} :
a ba - b 0

Alias of the reverse direction of sub_nonpos.

theorem le_sub_iff_add_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a c - b a + b c
theorem le_div_iff_mul_le {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a c / b a * b c
theorem add_le_of_le_sub_right {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a c - ba + b c

Alias of the forward direction of le_sub_iff_add_le.

theorem le_sub_right_of_add_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a + b ca c - b

Alias of the reverse direction of le_sub_iff_add_le.

theorem sub_le_iff_le_add {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a - c b a b + c
@[simp]
theorem div_le_iff_le_mul {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a / c b a b * c
@[instance 100]
instance AddGroup.toOrderedSub {α : Type u_1} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
Equations
  • =
theorem sub_le_sub_iff_left {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {b : α} {c : α} (a : α) :
a - b a - c c b
theorem div_le_div_iff_left {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {b : α} {c : α} (a : α) :
a / b a / c c b
theorem sub_le_sub_left {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} (h : a b) (c : α) :
c - b c - a
theorem div_le_div_left' {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} (h : a b) (c : α) :
c / b c / a
theorem sub_le_sub_iff {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} {d : α} :
a - b c - d a + d c + b
theorem div_le_div_iff' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} {d : α} :
a / b c / d a * d c * b
theorem le_sub_iff_add_le' {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
b c - a a + b c
theorem le_div_iff_mul_le' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
b c / a a * b c
theorem add_le_of_le_sub_left {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
b c - aa + b c

Alias of the forward direction of le_sub_iff_add_le'.

theorem le_sub_left_of_add_le {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a + b cb c - a

Alias of the reverse direction of le_sub_iff_add_le'.

theorem sub_le_iff_le_add' {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a - b c a b + c
theorem div_le_iff_le_mul' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a / b c a b * c
theorem sub_left_le_of_le_add {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a b + ca - b c

Alias of the reverse direction of sub_le_iff_le_add'.

theorem le_add_of_sub_left_le {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a - b ca b + c

Alias of the forward direction of sub_le_iff_le_add'.

@[simp]
theorem neg_le_sub_iff_le_add {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
-b a - c c a + b
@[simp]
theorem inv_le_div_iff_le_mul {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
b⁻¹ a / c c a * b
theorem neg_le_sub_iff_le_add' {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
-a b - c c a + b
theorem inv_le_div_iff_le_mul' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a⁻¹ b / c c a * b
theorem sub_le_comm {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a - b c a - c b
theorem div_le_comm {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a / b c a / c b
theorem le_sub_comm {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a b - c c b - a
theorem le_div_comm {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} :
a b / c c b / a
theorem sub_le_sub {α : Type u} [AddCommGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} {d : α} (hab : a b) (hcd : c d) :
a - d b - c
theorem div_le_div'' {α : Type u} [CommGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} {c : α} {d : α} (hab : a b) (hcd : c d) :
a / d b / c
@[simp]
theorem sub_lt_sub_iff_right {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (c : α) :
a - c < b - c a < b
@[simp]
theorem div_lt_div_iff_right {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (c : α) :
a / c < b / c a < b
theorem sub_lt_sub_right {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : a < b) (c : α) :
a - c < b - c
theorem div_lt_div_right' {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : a < b) (c : α) :
a / c < b / c
@[simp]
theorem sub_pos {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
0 < a - b b < a
@[simp]
theorem one_lt_div' {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
1 < a / b b < a
theorem sub_pos_of_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
b < a0 < a - b

Alias of the reverse direction of sub_pos.

theorem lt_of_sub_pos {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
0 < a - bb < a

Alias of the forward direction of sub_pos.

@[simp]
theorem sub_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a - b < 0 a < b

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

@[simp]
theorem div_lt_one' {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a / b < 1 a < b
theorem lt_of_sub_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a - b < 0a < b

Alias of the forward direction of sub_neg.


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

theorem sub_neg_of_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a < ba - b < 0

Alias of the reverse direction of sub_neg.


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

theorem sub_lt_zero {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} :
a - b < 0 a < b

Alias of sub_neg.


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

theorem lt_sub_iff_add_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a < c - b a + b < c
theorem lt_div_iff_mul_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a < c / b a * b < c
theorem add_lt_of_lt_sub_right {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a < c - ba + b < c

Alias of the forward direction of lt_sub_iff_add_lt.

theorem lt_sub_right_of_add_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a + b < ca < c - b

Alias of the reverse direction of lt_sub_iff_add_lt.

theorem sub_lt_iff_lt_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a - c < b a < b + c
theorem div_lt_iff_lt_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a / c < b a < b * c
theorem lt_add_of_sub_right_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a - c < ba < b + c

Alias of the forward direction of sub_lt_iff_lt_add.

theorem sub_right_lt_of_lt_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a < b + ca - c < b

Alias of the reverse direction of sub_lt_iff_lt_add.

@[simp]
theorem sub_lt_sub_iff_left {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {b : α} {c : α} (a : α) :
a - b < a - c c < b
@[simp]
theorem div_lt_div_iff_left {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {b : α} {c : α} (a : α) :
a / b < a / c c < b
@[simp]
theorem neg_lt_sub_iff_lt_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
-a < b - c c < a + b
@[simp]
theorem inv_lt_div_iff_lt_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a⁻¹ < b / c c < a * b
theorem sub_lt_sub_left {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : a < b) (c : α) :
c - b < c - a
theorem div_lt_div_left' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : a < b) (c : α) :
c / b < c / a
theorem sub_lt_sub_iff {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} :
a - b < c - d a + d < c + b
theorem div_lt_div_iff' {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} :
a / b < c / d a * d < c * b
theorem lt_sub_iff_add_lt' {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
b < c - a a + b < c
theorem lt_div_iff_mul_lt' {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
b < c / a a * b < c
theorem lt_sub_left_of_add_lt {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a + b < cb < c - a

Alias of the reverse direction of lt_sub_iff_add_lt'.

theorem add_lt_of_lt_sub_left {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
b < c - aa + b < c

Alias of the forward direction of lt_sub_iff_add_lt'.

theorem sub_lt_iff_lt_add' {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a - b < c a < b + c
theorem div_lt_iff_lt_mul' {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a / b < c a < b * c
theorem sub_left_lt_of_lt_add {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a < b + ca - b < c

Alias of the reverse direction of sub_lt_iff_lt_add'.

theorem lt_add_of_sub_left_lt {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} :
a - b < ca < b + c

Alias of the forward direction of sub_lt_iff_lt_add'.

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