Ordered groups

This file develops the basics of 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.

ink

class OrderedAddCommGroup (α : Type u) extends AddCommGroup , PartialOrder : Type u

• Addition is monotone in a ordered additive commutative group.

  add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b

An ordered additive commutative group is an additive commutative group with a partial order in which addition is strictly monotone.

ink

class OrderedCommGroup (α : Type u) extends CommGroup , PartialOrder : Type u

• Multiplication is monotone in a ordered commutative group.

  mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b

An ordered commutative group is an commutative group with a partial order in which multiplication is strictly monotone.

ink

def OrderedAddCommGroup.to_covariantClass_left_le.proof_1 (α : Type u_1) [inst : OrderedAddCommGroup α] : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• (_ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1) = (_ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1)

ink

instance OrderedAddCommGroup.to_covariantClass_left_le (α : Type u) [inst : OrderedAddCommGroup α] : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• OrderedAddCommGroup.to_covariantClass_left_le = OrderedAddCommGroup.to_covariantClass_left_le.proof_1

ink

instance OrderedCommGroup.to_covariantClass_left_le (α : Type u) [inst : OrderedCommGroup α] : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

• OrderedCommGroup.to_covariantClass_left_le = OrderedCommGroup.to_covariantClass_left_le.proof_1

ink

def OrderedAddCommGroup.toOrderedCancelAddCommMonoid.proof_2 {α : Type u_1} [inst : OrderedAddCommGroup α] (a : α) (b : α) (c : α) (bc : a + b ≤ a + c) : b ≤ c

Equations

• (_ : a + b ≤ a + c → b ≤ c) = (_ : a + b ≤ a + c → b ≤ c)

ink

instance OrderedAddCommGroup.toOrderedCancelAddCommMonoid {α : Type u} [inst : OrderedAddCommGroup α] : OrderedCancelAddCommMonoid α

Equations

• One or more equations did not get rendered due to their size.

ink

def OrderedAddCommGroup.toOrderedCancelAddCommMonoid.proof_1 {α : Type u_1} [inst : OrderedAddCommGroup α] (a : α) (b : α) : a + b = b + a

Equations

• (_ : ∀ (a b : α), a + b = b + a) = (_ : ∀ (a b : α), a + b = b + a)

ink

instance OrderedCommGroup.toOrderedCancelCommMonoid {α : Type u} [inst : OrderedCommGroup α] : OrderedCancelCommMonoid α

Equations

• OrderedCommGroup.toOrderedCancelCommMonoid = let src := inst; OrderedCancelCommMonoid.mk (_ : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b) (_ : ∀ (a b c : α), a * b ≤ a * c → b ≤ c)

ink

instance OrderedAddCommGroup.to_contravariantClass_left_le (α : Type u) [inst : OrderedAddCommGroup α] : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

A choice-free shortcut instance.

Equations

• OrderedAddCommGroup.to_contravariantClass_left_le = OrderedAddCommGroup.to_contravariantClass_left_le.proof_1

ink

def OrderedAddCommGroup.to_contravariantClass_left_le.proof_1 (α : Type u_1) [inst : OrderedAddCommGroup α] : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• (_ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1) = (_ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1)

ink

instance OrderedCommGroup.to_contravariantClass_left_le (α : Type u) [inst : OrderedCommGroup α] : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

A choice-free shortcut instance.

Equations

• OrderedCommGroup.to_contravariantClass_left_le = OrderedCommGroup.to_contravariantClass_left_le.proof_1

ink

def OrderedAddCommGroup.to_contravariantClass_right_le.proof_1 (α : Type u_1) [inst : OrderedAddCommGroup α] : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• (_ : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1) = (_ : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1)

ink

instance OrderedAddCommGroup.to_contravariantClass_right_le (α : Type u) [inst : OrderedAddCommGroup α] : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

A choice-free shortcut instance.

Equations

• OrderedAddCommGroup.to_contravariantClass_right_le = OrderedAddCommGroup.to_contravariantClass_right_le.proof_1

ink

instance OrderedCommGroup.to_contravariantClass_right_le (α : Type u) [inst : OrderedCommGroup α] : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

A choice-free shortcut instance.

Equations

• OrderedCommGroup.to_contravariantClass_right_le = OrderedCommGroup.to_contravariantClass_right_le.proof_1

ink

@[simp]

theorem Left.neg_nonpos_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} : -a ≤ 0 ↔ 0 ≤ a

Uses left co(ntra)variant.

ink

@[simp]

theorem Left.inv_le_one_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} : a⁻¹ ≤ 1 ↔ 1 ≤ a

Uses left co(ntra)variant.

ink

@[simp]

theorem Left.nonneg_neg_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} : 0 ≤ -a ↔ a ≤ 0

Uses left co(ntra)variant.

ink

@[simp]

theorem Left.one_le_inv_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} : 1 ≤ a⁻¹ ↔ a ≤ 1

Uses left co(ntra)variant.

ink

@[simp]

theorem le_neg_add_iff_add_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : b ≤ -a + c ↔ a + b ≤ c

ink

@[simp]

theorem le_inv_mul_iff_mul_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : b ≤ a⁻¹ * c ↔ a * b ≤ c

ink

@[simp]

theorem neg_add_le_iff_le_add {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : -b + a ≤ c ↔ a ≤ b + c

ink

@[simp]

theorem inv_mul_le_iff_le_mul {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : b⁻¹ * a ≤ c ↔ a ≤ b * c

ink

theorem neg_le_iff_add_nonneg' {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : -a ≤ b ↔ 0 ≤ a + b

ink

theorem inv_le_iff_one_le_mul' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a⁻¹ ≤ b ↔ 1 ≤ a * b

ink

theorem le_neg_iff_add_nonpos_left {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a ≤ -b ↔ b + a ≤ 0

ink

theorem le_inv_iff_mul_le_one_left {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a ≤ b⁻¹ ↔ b * a ≤ 1

ink

theorem le_neg_add_iff_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : 0 ≤ -b + a ↔ b ≤ a

ink

theorem le_inv_mul_iff_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : 1 ≤ b⁻¹ * a ↔ b ≤ a

ink

theorem neg_add_nonpos_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : -a + b ≤ 0 ↔ b ≤ a

ink

theorem inv_mul_le_one_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a⁻¹ * b ≤ 1 ↔ b ≤ a

ink

@[simp]

theorem Left.neg_pos_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} : 0 < -a ↔ a < 0

Uses left co(ntra)variant.

ink

@[simp]

theorem Left.one_lt_inv_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} : 1 < a⁻¹ ↔ a < 1

Uses left co(ntra)variant.

ink

@[simp]

theorem Left.neg_neg_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} : -a < 0 ↔ 0 < a

Uses left co(ntra)variant.

ink

@[simp]

theorem Left.inv_lt_one_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} : a⁻¹ < 1 ↔ 1 < a

Uses left co(ntra)variant.

ink

@[simp]

theorem lt_neg_add_iff_add_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : b < -a + c ↔ a + b < c

ink

@[simp]

theorem lt_inv_mul_iff_mul_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : b < a⁻¹ * c ↔ a * b < c

ink

@[simp]

theorem neg_add_lt_iff_lt_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : -b + a < c ↔ a < b + c

ink

@[simp]

theorem inv_mul_lt_iff_lt_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : b⁻¹ * a < c ↔ a < b * c

ink

theorem neg_lt_iff_pos_add' {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : -a < b ↔ 0 < a + b

ink

theorem inv_lt_iff_one_lt_mul' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a⁻¹ < b ↔ 1 < a * b

ink

theorem lt_neg_iff_add_neg' {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a < -b ↔ b + a < 0

ink

theorem lt_inv_iff_mul_lt_one' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a < b⁻¹ ↔ b * a < 1

ink

theorem lt_neg_add_iff_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : 0 < -b + a ↔ b < a

ink

theorem lt_inv_mul_iff_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : 1 < b⁻¹ * a ↔ b < a

ink

theorem neg_add_neg_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : -a + b < 0 ↔ b < a

ink

theorem inv_mul_lt_one_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a⁻¹ * b < 1 ↔ b < a

ink

@[simp]

theorem Right.neg_nonpos_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} : -a ≤ 0 ↔ 0 ≤ a

Uses right co(ntra)variant.

ink

@[simp]

theorem Right.inv_le_one_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} : a⁻¹ ≤ 1 ↔ 1 ≤ a

Uses right co(ntra)variant.

ink

@[simp]

theorem Right.nonneg_neg_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} : 0 ≤ -a ↔ a ≤ 0

Uses right co(ntra)variant.

ink

@[simp]

theorem Right.one_le_inv_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} : 1 ≤ a⁻¹ ↔ a ≤ 1

Uses right co(ntra)variant.

ink

theorem neg_le_iff_add_nonneg {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : -a ≤ b ↔ 0 ≤ b + a

ink

theorem inv_le_iff_one_le_mul {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a⁻¹ ≤ b ↔ 1 ≤ b * a

ink

theorem le_neg_iff_add_nonpos_right {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a ≤ -b ↔ a + b ≤ 0

ink

theorem le_inv_iff_mul_le_one_right {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a ≤ b⁻¹ ↔ a * b ≤ 1

ink

@[simp]

theorem add_neg_le_iff_le_add {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a + -b ≤ c ↔ a ≤ c + b

ink

@[simp]

theorem mul_inv_le_iff_le_mul {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a * b⁻¹ ≤ c ↔ a ≤ c * b

ink

@[simp]

theorem le_add_neg_iff_add_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : c ≤ a + -b ↔ c + b ≤ a

ink

@[simp]

theorem le_mul_inv_iff_mul_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : c ≤ a * b⁻¹ ↔ c * b ≤ a

ink

theorem add_neg_nonpos_iff_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a + -b ≤ 0 ↔ a ≤ b

ink

theorem mul_inv_le_one_iff_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a * b⁻¹ ≤ 1 ↔ a ≤ b

ink

theorem le_add_neg_iff_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : 0 ≤ a + -b ↔ b ≤ a

ink

theorem le_mul_inv_iff_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : 1 ≤ a * b⁻¹ ↔ b ≤ a

ink

theorem add_neg_nonpos_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : b + -a ≤ 0 ↔ b ≤ a

ink

theorem mul_inv_le_one_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : b * a⁻¹ ≤ 1 ↔ b ≤ a

ink

@[simp]

theorem Right.neg_neg_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} : -a < 0 ↔ 0 < a

Uses right co(ntra)variant.

ink

@[simp]

theorem Right.inv_lt_one_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} : a⁻¹ < 1 ↔ 1 < a

Uses right co(ntra)variant.

ink

@[simp]

theorem Right.neg_pos_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} : 0 < -a ↔ a < 0

Uses right co(ntra)variant.

ink

@[simp]

theorem Right.one_lt_inv_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} : 1 < a⁻¹ ↔ a < 1

Uses right co(ntra)variant.

ink

theorem neg_lt_iff_pos_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : -a < b ↔ 0 < b + a

ink

theorem inv_lt_iff_one_lt_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a⁻¹ < b ↔ 1 < b * a

ink

theorem lt_neg_iff_add_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a < -b ↔ a + b < 0

ink

theorem lt_inv_iff_mul_lt_one {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a < b⁻¹ ↔ a * b < 1

ink

@[simp]

theorem add_neg_lt_iff_lt_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a + -b < c ↔ a < c + b

ink

@[simp]

theorem mul_inv_lt_iff_lt_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a * b⁻¹ < c ↔ a < c * b

ink

@[simp]

theorem lt_add_neg_iff_add_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : c < a + -b ↔ c + b < a

ink

@[simp]

theorem lt_mul_inv_iff_mul_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : c < a * b⁻¹ ↔ c * b < a

ink

theorem neg_add_neg_iff_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a + -b < 0 ↔ a < b

ink

theorem inv_mul_lt_one_iff_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a * b⁻¹ < 1 ↔ a < b

ink

theorem lt_add_neg_iff_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : 0 < a + -b ↔ b < a

ink

theorem lt_mul_inv_iff_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : 1 < a * b⁻¹ ↔ b < a

ink

theorem add_neg_neg_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : b + -a < 0 ↔ b < a

ink

theorem mul_inv_lt_one_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : b * a⁻¹ < 1 ↔ b < a

ink

@[simp]

theorem neg_le_neg_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : -a ≤ -b ↔ b ≤ a

ink

@[simp]

theorem inv_le_inv_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a⁻¹ ≤ b⁻¹ ↔ b ≤ a

ink

theorem le_of_neg_le_neg {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : -a ≤ -b → b ≤ a

Alias of the forward direction of neg_le_neg_iff.

ink

theorem add_neg_le_neg_add_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} : a + -b ≤ -d + c ↔ d + a ≤ c + b

ink

theorem mul_inv_le_inv_mul_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} : a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b

ink

@[simp]

theorem sub_le_self_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} : a - b ≤ a ↔ 0 ≤ b

ink

@[simp]

theorem div_le_self_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} : a / b ≤ a ↔ 1 ≤ b

ink

@[simp]

theorem le_sub_self_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} : a ≤ a - b ↔ b ≤ 0

ink

@[simp]

theorem le_div_self_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} : a ≤ a / b ↔ b ≤ 1

ink

theorem sub_le_self {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} : 0 ≤ b → a - b ≤ a

Alias of the reverse direction of sub_le_self_iff.

ink

@[simp]

theorem neg_lt_neg_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : -a < -b ↔ b < a

ink

@[simp]

theorem inv_lt_inv_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a⁻¹ < b⁻¹ ↔ b < a

ink

theorem neg_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : -a < b ↔ -b < a

ink

theorem inv_lt' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a⁻¹ < b ↔ b⁻¹ < a

ink

theorem lt_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a < -b ↔ b < -a

ink

theorem lt_inv' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a < b⁻¹ ↔ b < a⁻¹

ink

theorem lt_inv_of_lt_inv {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a < b⁻¹ → b < a⁻¹

Alias of the forward direction of lt_inv'.

ink

theorem lt_neg_of_lt_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a < -b → b < -a

ink

theorem inv_lt_of_inv_lt' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a⁻¹ < b → b⁻¹ < a

Alias of the forward direction of inv_lt'.

ink

theorem neg_lt_of_neg_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : -a < b → -b < a

ink

theorem add_neg_lt_neg_add_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} : a + -b < -d + c ↔ d + a < c + b

ink

theorem mul_inv_lt_inv_mul_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} : a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b

ink

@[simp]

theorem sub_lt_self_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α} : a - b < a ↔ 0 < b

ink

@[simp]

theorem div_lt_self_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) {b : α} : a / b < a ↔ 1 < b

ink

theorem sub_lt_self {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α} : 0 < b → a - b < a

Alias of the reverse direction of sub_lt_self_iff.

ink

theorem Left.neg_le_self {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} (h : 0 ≤ a) : -a ≤ a

ink

theorem Left.inv_le_self {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} (h : 1 ≤ a) : a⁻¹ ≤ a

ink

theorem neg_le_self {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} (h : 0 ≤ a) : -a ≤ a

Alias of Left.neg_le_self.

ink

theorem Left.self_le_neg {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} (h : a ≤ 0) : a ≤ -a

ink

theorem Left.self_le_inv {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} (h : a ≤ 1) : a ≤ a⁻¹

ink

theorem Left.neg_lt_self {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} (h : 0 < a) : -a < a

ink

theorem Left.inv_lt_self {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} (h : 1 < a) : a⁻¹ < a

ink

theorem neg_lt_self {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} (h : 0 < a) : -a < a

Alias of Left.neg_lt_self.

ink

theorem Left.self_lt_neg {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} (h : a < 0) : a < -a

ink

theorem Left.self_lt_inv {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} (h : a < 1) : a < a⁻¹

ink

theorem Right.neg_le_self {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} (h : 0 ≤ a) : -a ≤ a

ink

theorem Right.inv_le_self {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} (h : 1 ≤ a) : a⁻¹ ≤ a

ink

theorem Right.self_le_neg {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} (h : a ≤ 0) : a ≤ -a

ink

theorem Right.self_le_inv {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} (h : a ≤ 1) : a ≤ a⁻¹

ink

theorem Right.neg_lt_self {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} (h : 0 < a) : -a < a

ink

theorem Right.inv_lt_self {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} (h : 1 < a) : a⁻¹ < a

ink

theorem Right.self_lt_neg {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} (h : a < 0) : a < -a

ink

theorem Right.self_lt_inv {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} (h : a < 1) : a < a⁻¹

ink

theorem neg_add_le_iff_le_add' {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : -c + a ≤ b ↔ a ≤ b + c

ink

theorem inv_mul_le_iff_le_mul' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : c⁻¹ * a ≤ b ↔ a ≤ b * c

ink

theorem add_neg_le_iff_le_add' {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a + -b ≤ c ↔ a ≤ b + c

ink

theorem mul_inv_le_iff_le_mul' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a * b⁻¹ ≤ c ↔ a ≤ b * c

ink

theorem add_neg_le_add_neg_iff {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} : a + -b ≤ c + -d ↔ a + d ≤ c + b

ink

theorem mul_inv_le_mul_inv_iff' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b

ink

theorem neg_add_lt_iff_lt_add' {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : -c + a < b ↔ a < b + c

ink

theorem inv_mul_lt_iff_lt_mul' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : c⁻¹ * a < b ↔ a < b * c

ink

theorem add_neg_lt_iff_le_add' {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a + -b < c ↔ a < b + c

ink

theorem mul_inv_lt_iff_le_mul' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a * b⁻¹ < c ↔ a < b * c

ink

theorem add_neg_lt_add_neg_iff {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} : a + -b < c + -d ↔ a + d < c + b

ink

theorem mul_inv_lt_mul_inv_iff' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} : a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b

ink

theorem one_le_of_inv_le_one {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} : a⁻¹ ≤ 1 → 1 ≤ a

Alias of the forward direction of Left.inv_le_one_iff.

ink

theorem nonneg_of_neg_nonpos {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} : -a ≤ 0 → 0 ≤ a

ink

theorem le_one_of_one_le_inv {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} : 1 ≤ a⁻¹ → a ≤ 1

Alias of the forward direction of Left.one_le_inv_iff.

ink

theorem nonpos_of_neg_nonneg {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} : 0 ≤ -a → a ≤ 0

ink

theorem lt_of_inv_lt_inv {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a⁻¹ < b⁻¹ → b < a

Alias of the forward direction of inv_lt_inv_iff.

ink

theorem lt_of_neg_lt_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : -a < -b → b < a

ink

theorem one_lt_of_inv_lt_one {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} : a⁻¹ < 1 → 1 < a

Alias of the forward direction of Left.inv_lt_one_iff.

ink

theorem pos_of_neg_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} : -a < 0 → 0 < a

ink

theorem inv_lt_one_iff_one_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} : a⁻¹ < 1 ↔ 1 < a

Alias of Left.inv_lt_one_iff.

ink

theorem neg_neg_iff_pos {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} : -a < 0 ↔ 0 < a

ink

theorem inv_lt_one' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} : a⁻¹ < 1 ↔ 1 < a

Alias of Left.inv_lt_one_iff.

ink

theorem neg_lt_zero {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} : -a < 0 ↔ 0 < a

ink

theorem inv_of_one_lt_inv {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} : 1 < a⁻¹ → a < 1

Alias of the forward direction of Left.one_lt_inv_iff.

ink

theorem neg_of_neg_pos {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} : 0 < -a → a < 0

ink

theorem one_lt_inv_of_inv {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} : a < 1 → 1 < a⁻¹

Alias of the reverse direction of Left.one_lt_inv_iff.

ink

theorem neg_pos_of_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} : a < 0 → 0 < -a

ink

theorem mul_le_of_le_inv_mul {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : b ≤ a⁻¹ * c → a * b ≤ c

Alias of the forward direction of le_inv_mul_iff_mul_le.

ink

theorem add_le_of_le_neg_add {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : b ≤ -a + c → a + b ≤ c

ink

theorem le_inv_mul_of_mul_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a * b ≤ c → b ≤ a⁻¹ * c

Alias of the reverse direction of le_inv_mul_iff_mul_le.

ink

theorem le_neg_add_of_add_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a + b ≤ c → b ≤ -a + c

ink

theorem inv_mul_le_of_le_mul {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a ≤ b * c → b⁻¹ * a ≤ c

Alias of the reverse direction of inv_mul_le_iff_le_mul.

ink

theorem neg_add_le_of_le_add {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a ≤ b + c → -b + a ≤ c

ink

theorem mul_lt_of_lt_inv_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : b < a⁻¹ * c → a * b < c

Alias of the forward direction of lt_inv_mul_iff_mul_lt.

ink

theorem add_lt_of_lt_neg_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : b < -a + c → a + b < c

ink

theorem lt_inv_mul_of_mul_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a * b < c → b < a⁻¹ * c

Alias of the reverse direction of lt_inv_mul_iff_mul_lt.

ink

theorem lt_neg_add_of_add_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a + b < c → b < -a + c

ink

theorem lt_mul_of_inv_mul_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : b⁻¹ * a < c → a < b * c

Alias of the forward direction of inv_mul_lt_iff_lt_mul.

ink

theorem inv_mul_lt_of_lt_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a < b * c → b⁻¹ * a < c

Alias of the reverse direction of inv_mul_lt_iff_lt_mul.

ink

theorem lt_add_of_neg_add_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : -b + a < c → a < b + c

ink

theorem neg_add_lt_of_lt_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a < b + c → -b + a < c

ink

theorem lt_mul_of_inv_mul_lt_left {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : b⁻¹ * a < c → a < b * c

Alias of lt_mul_of_inv_mul_lt.

ink

theorem lt_add_of_neg_add_lt_left {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : -b + a < c → a < b + c

ink

theorem inv_le_one' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} : a⁻¹ ≤ 1 ↔ 1 ≤ a

Alias of Left.inv_le_one_iff.

ink

theorem neg_nonpos {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} : -a ≤ 0 ↔ 0 ≤ a

ink

theorem one_le_inv' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} : 1 ≤ a⁻¹ ↔ a ≤ 1

Alias of Left.one_le_inv_iff.

ink

theorem neg_nonneg {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} : 0 ≤ -a ↔ a ≤ 0

ink

theorem one_lt_inv' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} : 1 < a⁻¹ ↔ a < 1

Alias of Left.one_lt_inv_iff.

ink

theorem neg_pos {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} : 0 < -a ↔ a < 0

ink

theorem OrderedCommGroup.mul_lt_mul_left' {α : Type u_1} [inst : Mul α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {b : α} {c : α} (bc : b < c) (a : α) : a * b < a * c

Alias of mul_lt_mul_left'.

ink

theorem OrderedAddCommGroup.add_lt_add_left {α : Type u_1} [inst : Add α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {b : α} {c : α} (bc : b < c) (a : α) : a + b < a + c

ink

theorem OrderedCommGroup.le_of_mul_le_mul_left {α : Type u_1} [inst : Mul α] [inst : LE α] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (bc : a * b ≤ a * c) : b ≤ c

Alias of le_of_mul_le_mul_left'.

ink

theorem OrderedAddCommGroup.le_of_add_le_add_left {α : Type u_1} [inst : Add α] [inst : LE α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (bc : a + b ≤ a + c) : b ≤ c

ink

theorem OrderedCommGroup.lt_of_mul_lt_mul_left {α : Type u_1} [inst : Mul α] [inst : LT α] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (bc : a * b < a * c) : b < c

Alias of lt_of_mul_lt_mul_left'.

ink

theorem OrderedAddCommGroup.lt_of_add_lt_add_left {α : Type u_1} [inst : Add α] [inst : LT α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (bc : a + b < a + c) : b < c

ink

@[simp]

theorem sub_le_sub_iff_right {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (c : α) : a - c ≤ b - c ↔ a ≤ b

ink

@[simp]

theorem div_le_div_iff_right {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (c : α) : a / c ≤ b / c ↔ a ≤ b

ink

theorem sub_le_sub_right {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : a ≤ b) (c : α) : a - c ≤ b - c

ink

theorem div_le_div_right' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : a ≤ b) (c : α) : a / c ≤ b / c

ink

@[simp]

theorem sub_nonneg {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : 0 ≤ a - b ↔ b ≤ a

ink

@[simp]

theorem one_le_div' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : 1 ≤ a / b ↔ b ≤ a

ink

theorem sub_nonneg_of_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : b ≤ a → 0 ≤ a - b

Alias of the reverse direction of sub_nonneg.

ink

theorem le_of_sub_nonneg {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : 0 ≤ a - b → b ≤ a

Alias of the forward direction of sub_nonneg.

ink

@[simp]

theorem sub_nonpos {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a - b ≤ 0 ↔ a ≤ b

ink

@[simp]

theorem div_le_one' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a / b ≤ 1 ↔ a ≤ b

ink

theorem sub_nonpos_of_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a ≤ b → a - b ≤ 0

Alias of the reverse direction of sub_nonpos.

ink

theorem le_of_sub_nonpos {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a - b ≤ 0 → a ≤ b

Alias of the forward direction of sub_nonpos.

ink

theorem le_sub_iff_add_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a ≤ c - b ↔ a + b ≤ c

ink

theorem le_div_iff_mul_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a ≤ c / b ↔ a * b ≤ c

ink

theorem le_sub_right_of_add_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a + b ≤ c → a ≤ c - b

Alias of the reverse direction of le_sub_iff_add_le.

ink

theorem add_le_of_le_sub_right {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a ≤ c - b → a + b ≤ c

Alias of the forward direction of le_sub_iff_add_le.

ink

theorem sub_le_iff_le_add {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a - c ≤ b ↔ a ≤ b + c

ink

theorem div_le_iff_le_mul {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a / c ≤ b ↔ a ≤ b * c

ink

instance AddGroup.toHasOrderedSub {α : Type u_1} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] : OrderedSub α

Equations

• AddGroup.toHasOrderedSub = { tsub_le_iff_right := (_ : ∀ (x x_1 x_2 : α), x - x_1 ≤ x_2 ↔ x ≤ x_2 + x_1) }

ink

@[simp]

theorem sub_le_sub_iff_left {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b : α} {c : α} (a : α) : a - b ≤ a - c ↔ c ≤ b

ink

@[simp]

theorem div_le_div_iff_left {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {b : α} {c : α} (a : α) : a / b ≤ a / c ↔ c ≤ b

ink

theorem sub_le_sub_left {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : a ≤ b) (c : α) : c - b ≤ c - a

ink

theorem div_le_div_left' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : a ≤ b) (c : α) : c / b ≤ c / a

ink

theorem sub_le_sub_iff {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} : a - b ≤ c - d ↔ a + d ≤ c + b

ink

theorem div_le_div_iff' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} : a / b ≤ c / d ↔ a * d ≤ c * b

ink

theorem le_sub_iff_add_le' {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : b ≤ c - a ↔ a + b ≤ c

ink

theorem le_div_iff_mul_le' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : b ≤ c / a ↔ a * b ≤ c

ink

theorem add_le_of_le_sub_left {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : b ≤ c - a → a + b ≤ c

Alias of the forward direction of le_sub_iff_add_le'.

ink

theorem le_sub_left_of_add_le {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a + b ≤ c → b ≤ c - a

Alias of the reverse direction of le_sub_iff_add_le'.

ink

theorem sub_le_iff_le_add' {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a - b ≤ c ↔ a ≤ b + c

ink

theorem div_le_iff_le_mul' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a / b ≤ c ↔ a ≤ b * c

ink

theorem sub_left_le_of_le_add {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a ≤ b + c → a - b ≤ c

Alias of the reverse direction of sub_le_iff_le_add'.

ink

theorem le_add_of_sub_left_le {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a - b ≤ c → a ≤ b + c

Alias of the forward direction of sub_le_iff_le_add'.

ink

@[simp]

theorem neg_le_sub_iff_le_add {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : -b ≤ a - c ↔ c ≤ a + b

ink

@[simp]

theorem inv_le_div_iff_le_mul {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : b⁻¹ ≤ a / c ↔ c ≤ a * b

ink

theorem neg_le_sub_iff_le_add' {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : -a ≤ b - c ↔ c ≤ a + b

ink

theorem inv_le_div_iff_le_mul' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a⁻¹ ≤ b / c ↔ c ≤ a * b

ink

theorem sub_le_comm {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a - b ≤ c ↔ a - c ≤ b

ink

theorem div_le_comm {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a / b ≤ c ↔ a / c ≤ b

ink

theorem le_sub_comm {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a ≤ b - c ↔ c ≤ b - a

ink

theorem le_div_comm {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} : a ≤ b / c ↔ c ≤ b / a

ink

theorem sub_le_sub {α : Type u} [inst : AddCommGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c

ink

theorem div_le_div'' {α : Type u} [inst : CommGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (hab : a ≤ b) (hcd : c ≤ d) : a / d ≤ b / c

ink

@[simp]

theorem sub_lt_sub_iff_right {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (c : α) : a - c < b - c ↔ a < b

ink

@[simp]

theorem div_lt_div_iff_right {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (c : α) : a / c < b / c ↔ a < b

ink

theorem sub_lt_sub_right {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a < b) (c : α) : a - c < b - c

ink

theorem div_lt_div_right' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a < b) (c : α) : a / c < b / c

ink

@[simp]

theorem sub_pos {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : 0 < a - b ↔ b < a

ink

@[simp]

theorem one_lt_div' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : 1 < a / b ↔ b < a

ink

theorem sub_pos_of_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : b < a → 0 < a - b

Alias of the reverse direction of sub_pos.

ink

theorem lt_of_sub_pos {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : 0 < a - b → b < a

Alias of the forward direction of sub_pos.

ink

@[simp]

theorem sub_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a - b < 0 ↔ a < b

ink

@[simp]

theorem div_lt_one' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a / b < 1 ↔ a < b

ink

theorem lt_of_sub_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a - b < 0 → a < b

Alias of the forward direction of sub_neg.

ink

theorem sub_neg_of_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a < b → a - b < 0

Alias of the reverse direction of sub_neg.

ink

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

Alias of sub_neg.

ink

theorem lt_sub_iff_add_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a < c - b ↔ a + b < c

ink

theorem lt_div_iff_mul_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a < c / b ↔ a * b < c

ink

theorem lt_sub_right_of_add_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a + b < c → a < c - b

Alias of the reverse direction of lt_sub_iff_add_lt.

ink

theorem add_lt_of_lt_sub_right {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a < c - b → a + b < c

Alias of the forward direction of lt_sub_iff_add_lt.

ink

theorem sub_lt_iff_lt_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a - c < b ↔ a < b + c

ink

theorem div_lt_iff_lt_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a / c < b ↔ a < b * c

ink

theorem sub_right_lt_of_lt_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a < b + c → a - c < b

Alias of the reverse direction of sub_lt_iff_lt_add.

ink

theorem lt_add_of_sub_right_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a - c < b → a < b + c

Alias of the forward direction of sub_lt_iff_lt_add.

ink

@[simp]

theorem sub_lt_sub_iff_left {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {b : α} {c : α} (a : α) : a - b < a - c ↔ c < b

ink

@[simp]

theorem div_lt_div_iff_left {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {b : α} {c : α} (a : α) : a / b < a / c ↔ c < b

ink

@[simp]

theorem neg_lt_sub_iff_lt_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : -a < b - c ↔ c < a + b

ink

@[simp]

theorem inv_lt_div_iff_lt_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a⁻¹ < b / c ↔ c < a * b

ink

theorem sub_lt_sub_left {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a < b) (c : α) : c - b < c - a

ink

theorem div_lt_div_left' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a < b) (c : α) : c / b < c / a

ink

theorem sub_lt_sub_iff {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} : a - b < c - d ↔ a + d < c + b

ink

theorem div_lt_div_iff' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} : a / b < c / d ↔ a * d < c * b

ink

theorem lt_sub_iff_add_lt' {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : b < c - a ↔ a + b < c

ink

theorem lt_div_iff_mul_lt' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : b < c / a ↔ a * b < c

ink

theorem lt_sub_left_of_add_lt {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a + b < c → b < c - a

Alias of the reverse direction of lt_sub_iff_add_lt'.

ink

theorem add_lt_of_lt_sub_left {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : b < c - a → a + b < c

Alias of the forward direction of lt_sub_iff_add_lt'.

ink

theorem sub_lt_iff_lt_add' {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a - b < c ↔ a < b + c

ink

theorem div_lt_iff_lt_mul' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a / b < c ↔ a < b * c

ink

theorem lt_add_of_sub_left_lt {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a - b < c → a < b + c

Alias of the forward direction of sub_lt_iff_lt_add'.

ink

theorem sub_left_lt_of_lt_add {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a < b + c → a - b < c

Alias of the reverse direction of sub_lt_iff_lt_add'.

ink

theorem neg_lt_sub_iff_lt_add' {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : -b < a - c ↔ c < a + b

ink

theorem inv_lt_div_iff_lt_mul' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : b⁻¹ < a / c ↔ c < a * b

ink

theorem sub_lt_comm {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a - b < c ↔ a - c < b

ink

theorem div_lt_comm {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a / b < c ↔ a / c < b

ink

theorem lt_sub_comm {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a < b - c ↔ c < b - a

ink

theorem lt_div_comm {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} : a < b / c ↔ c < b / a

ink

theorem sub_lt_sub {α : Type u} [inst : AddCommGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} (hab : a < b) (hcd : c < d) : a - d < b - c

ink

theorem div_lt_div'' {α : Type u} [inst : CommGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} (hab : a < b) (hcd : c < d) : a / d < b / c

ink

@[simp]

theorem cmp_sub_zero {α : Type u} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) : cmp (a - b) 0 = cmp a b

ink

@[simp]

theorem cmp_div_one' {α : Type u} [inst : Group α] [inst : LinearOrder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) : cmp (a / b) 1 = cmp a b

ink

theorem le_of_forall_pos_lt_add {α : Type u} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : ∀ (ε : α), 0 < ε → a < b + ε) : a ≤ b

ink

theorem le_of_forall_one_lt_lt_mul {α : Type u} [inst : Group α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : ∀ (ε : α), 1 < ε → a < b * ε) : a ≤ b

ink

theorem le_iff_forall_pos_lt_add {α : Type u} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a ≤ b ↔ ∀ (ε : α), 0 < ε → a < b + ε

ink

theorem le_iff_forall_one_lt_lt_mul {α : Type u} [inst : Group α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε

ink

theorem sub_le_neg_add_iff {α : Type u} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] : a - b ≤ -a + b ↔ a ≤ b

ink

theorem div_le_inv_mul_iff {α : Type u} [inst : Group α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] : a / b ≤ a⁻¹ * b ↔ a ≤ b

ink

theorem sub_le_sub_flip {α : Type u_1} [inst : AddCommGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a - b ≤ b - a ↔ a ≤ b

ink

@[simp]

theorem div_le_div_flip {α : Type u_1} [inst : CommGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a / b ≤ b / a ↔ a ≤ b

Linearly ordered commutative groups

ink

class LinearOrderedAddCommGroup (α : Type u) extends OrderedAddCommGroup , Min , Max , Ord : Type u

• A linear order is total.

  le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_le : DecidableRel fun x x_1 => x ≤ x_1

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_eq : DecidableEq α

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_lt : DecidableRel fun x x_1 => x < x_1

• The minimum function is equivalent to the one you get from minOfLe.

  min_def : autoParam (∀ (a b : α), min a b = if a ≤ b then a else b) _auto✝

• The minimum function is equivalent to the one you get from maxOfLe.

  max_def : autoParam (∀ (a b : α), max a b = if a ≤ b then b else a) _auto✝

• Comparison via compare is equal to the canonical comparison given decidable < and =.

  compare_eq_compareOfLessAndEq : autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b) _auto✝

A linearly ordered additive commutative group is an additive commutative group with a linear order in which addition is monotone.

ink

class LinearOrderedAddCommGroupWithTop (α : Type u_1) extends LinearOrderedAddCommMonoidWithTop , Neg , Sub , Nontrivial : Type u_1

• zsmul : ℤ → α → α
• zsmul_zero' : autoParam (∀ (a : α), zsmul 0 a = 0) _auto✝
• zsmul_succ' : autoParam (∀ (n : ℕ) (a : α), zsmul (Int.ofNat (Nat.succ n)) a = a + zsmul (Int.ofNat n) a) _auto✝
• zsmul_neg' : autoParam (∀ (n : ℕ) (a : α), zsmul (Int.negSucc n) a = -zsmul (↑(Nat.succ n)) a) _auto✝
• toNontrivial : Nontrivial α
• neg_top : -⊤ = ⊤
• add_neg_cancel : ∀ (a : α), a ≠ ⊤ → a + -a = 0

A linearly ordered commutative monoid with an additively absorbing ⊤ element. Instances should include number systems with an infinite element adjoined.`

ink

class LinearOrderedCommGroup (α : Type u) extends OrderedCommGroup , Min , Max , Ord : Type u

• A linear order is total.

  le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_le : DecidableRel fun x x_1 => x ≤ x_1

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_eq : DecidableEq α

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_lt : DecidableRel fun x x_1 => x < x_1

• The minimum function is equivalent to the one you get from minOfLe.

  min_def : autoParam (∀ (a b : α), min a b = if a ≤ b then a else b) _auto✝

• The minimum function is equivalent to the one you get from maxOfLe.

  max_def : autoParam (∀ (a b : α), max a b = if a ≤ b then b else a) _auto✝

• Comparison via compare is equal to the canonical comparison given decidable < and =.

  compare_eq_compareOfLessAndEq : autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b) _auto✝

A linearly ordered commutative group is a commutative group with a linear order in which multiplication is monotone.

ink

theorem LinearOrderedAddCommGroup.add_lt_add_left {α : Type u} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (h : a < b) (c : α) : c + a < c + b

ink

theorem LinearOrderedCommGroup.mul_lt_mul_left' {α : Type u} [inst : LinearOrderedCommGroup α] (a : α) (b : α) (h : a < b) (c : α) : c * a < c * b

ink

abbrev eq_zero_of_neg_eq.match_1 {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} (motive : a < 0 ∨ a = 0 ∨ 0 < a → Prop) : (x : a < 0 ∨ a = 0 ∨ 0 < a) → ((h₁ : a < 0) → motive (_ : a < 0 ∨ a = 0 ∨ 0 < a)) → ((h₁ : a = 0) → motive (_ : a < 0 ∨ a = 0 ∨ 0 < a)) → ((h₁ : 0 < a) → motive (_ : a < 0 ∨ a = 0 ∨ 0 < a)) → motive x

Equations

• eq_zero_of_neg_eq.match_1 motive x h_1 h_2 h_3 = Or.casesOn x (fun h => h_1 h) fun h => Or.casesOn h (fun h => h_2 h) fun h => h_3 h

ink

theorem eq_zero_of_neg_eq {α : Type u} [inst : LinearOrderedAddCommGroup α] {a : α} (h : -a = a) : a = 0

ink

theorem eq_one_of_inv_eq' {α : Type u} [inst : LinearOrderedCommGroup α] {a : α} (h : a⁻¹ = a) : a = 1

ink

theorem exists_zero_lt {α : Type u} [inst : LinearOrderedAddCommGroup α] [inst : Nontrivial α] : ∃ a, 0 < a

ink

theorem exists_one_lt' {α : Type u} [inst : LinearOrderedCommGroup α] [inst : Nontrivial α] : ∃ a, 1 < a

ink

instance LinearOrderedAddCommGroup.to_noMaxOrder {α : Type u} [inst : LinearOrderedAddCommGroup α] [inst : Nontrivial α] : NoMaxOrder α

Equations

• @LinearOrderedAddCommGroup.to_noMaxOrder = @LinearOrderedAddCommGroup.to_noMaxOrder.proof_1

ink

def LinearOrderedAddCommGroup.to_noMaxOrder.proof_1 {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [inst : Nontrivial α] : NoMaxOrder α

Equations

• (_ : NoMaxOrder α) = (_ : NoMaxOrder α)

ink

instance LinearOrderedCommGroup.to_noMaxOrder {α : Type u} [inst : LinearOrderedCommGroup α] [inst : Nontrivial α] : NoMaxOrder α

Equations

• @LinearOrderedCommGroup.to_noMaxOrder = @LinearOrderedCommGroup.to_noMaxOrder.proof_1

ink

def LinearOrderedAddCommGroup.to_noMinOrder.proof_1 {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [inst : Nontrivial α] : NoMinOrder α

Equations

• (_ : NoMinOrder α) = (_ : NoMinOrder α)

ink

instance LinearOrderedAddCommGroup.to_noMinOrder {α : Type u} [inst : LinearOrderedAddCommGroup α] [inst : Nontrivial α] : NoMinOrder α

Equations

• @LinearOrderedAddCommGroup.to_noMinOrder = @LinearOrderedAddCommGroup.to_noMinOrder.proof_1

ink

instance LinearOrderedCommGroup.to_noMinOrder {α : Type u} [inst : LinearOrderedCommGroup α] [inst : Nontrivial α] : NoMinOrder α

Equations

• @LinearOrderedCommGroup.to_noMinOrder = @LinearOrderedCommGroup.to_noMinOrder.proof_1

ink

def LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b

Equations

• (_ : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b) = (_ : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b)

ink

instance LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid {α : Type u} [inst : LinearOrderedAddCommGroup α] : LinearOrderedCancelAddCommMonoid α

Equations

• One or more equations did not get rendered due to their size.

ink

instance LinearOrderedCommGroup.toLinearOrderedCancelCommMonoid {α : Type u} [inst : LinearOrderedCommGroup α] : LinearOrderedCancelCommMonoid α

Equations

• One or more equations did not get rendered due to their size.

ink

structure AddCommGroup.PositiveCone (α : Type u_1) [inst : AddCommGroup α] : Type u_1

• nonneg : α → Prop
• pos : α → Prop
• pos_iff : autoParam (∀ (a : α), pos a ↔ nonneg a ∧ ¬nonneg (-a)) _auto✝
• zero_nonneg : nonneg 0
• add_nonneg : {a b : α} → nonneg a → nonneg b → nonneg (a + b)
• nonneg_antisymm : ∀ {a : α}, nonneg a → nonneg (-a) → a = 0

A collection of elements in an AddCommGroup designated as "non-negative". This is useful for constructing an OrderedAddCommGroup by choosing a positive cone in an exisiting AddCommGroup.

ink

structure AddCommGroup.TotalPositiveCone (α : Type u_1) [inst : AddCommGroup α] extends AddCommGroup.PositiveCone : Type u_1

• For any a the proposition nonneg a is decidable

  nonnegDecidable : DecidablePred toPositiveCone.nonneg

• Either a or -a is nonneg

  nonneg_total : ∀ (a : α), AddCommGroup.PositiveCone.nonneg toPositiveCone a ∨ AddCommGroup.PositiveCone.nonneg toPositiveCone (-a)

A positive cone in an AddCommGroup induces a linear order if for every a, either a or -a is non-negative.

ink

def OrderedAddCommGroup.mkOfPositiveCone {α : Type u_1} [inst : AddCommGroup α] (C : AddCommGroup.PositiveCone α) : OrderedAddCommGroup α

Construct an OrderedAddCommGroup by designating a positive cone in an existing AddCommGroup.

Equations

• OrderedAddCommGroup.mkOfPositiveCone C = let src := inst; OrderedAddCommGroup.mk (_ : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b)

ink

def LinearOrderedAddCommGroup.mkOfPositiveCone {α : Type u_1} [inst : AddCommGroup α] (C : AddCommGroup.TotalPositiveCone α) : LinearOrderedAddCommGroup α

Construct a LinearOrderedAddCommGroup by designating a positive cone in an existing AddCommGroup such that for every a, either a or -a is non-negative.

Equations

• One or more equations did not get rendered due to their size.

ink

theorem neg_le_neg {α : Type u} [inst : OrderedAddCommGroup α] {a : α} {b : α} : a ≤ b → -b ≤ -a

ink

theorem inv_le_inv' {α : Type u} [inst : OrderedCommGroup α] {a : α} {b : α} : a ≤ b → b⁻¹ ≤ a⁻¹

ink

theorem neg_lt_neg {α : Type u} [inst : OrderedAddCommGroup α] {a : α} {b : α} : a < b → -b < -a

ink

theorem inv_lt_inv' {α : Type u} [inst : OrderedCommGroup α] {a : α} {b : α} : a < b → b⁻¹ < a⁻¹

ink

theorem neg_neg_of_pos {α : Type u} [inst : OrderedAddCommGroup α] {a : α} : 0 < a → -a < 0

ink

theorem inv_lt_one_of_one_lt {α : Type u} [inst : OrderedCommGroup α] {a : α} : 1 < a → a⁻¹ < 1

ink

theorem neg_nonpos_of_nonneg {α : Type u} [inst : OrderedAddCommGroup α] {a : α} : 0 ≤ a → -a ≤ 0

ink

theorem inv_le_one_of_one_le {α : Type u} [inst : OrderedCommGroup α] {a : α} : 1 ≤ a → a⁻¹ ≤ 1

ink

theorem neg_nonneg_of_nonpos {α : Type u} [inst : OrderedAddCommGroup α] {a : α} : a ≤ 0 → 0 ≤ -a

ink

theorem one_le_inv_of_le_one {α : Type u} [inst : OrderedCommGroup α] {a : α} : a ≤ 1 → 1 ≤ a⁻¹

ink

theorem Monotone.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : Preorder β] {f : β → α} (hf : Monotone f) : Antitone fun x => -f x

ink

theorem Monotone.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : Preorder β] {f : β → α} (hf : Monotone f) : Antitone fun x => (f x)⁻¹

ink

theorem Antitone.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : Preorder β] {f : β → α} (hf : Antitone f) : Monotone fun x => -f x

ink

theorem Antitone.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : Preorder β] {f : β → α} (hf : Antitone f) : Monotone fun x => (f x)⁻¹

ink

theorem MonotoneOn.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : Preorder β] {f : β → α} {s : Set β} (hf : MonotoneOn f s) : AntitoneOn (fun x => -f x) s

ink

theorem MonotoneOn.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : Preorder β] {f : β → α} {s : Set β} (hf : MonotoneOn f s) : AntitoneOn (fun x => (f x)⁻¹) s

ink

theorem AntitoneOn.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : Preorder β] {f : β → α} {s : Set β} (hf : AntitoneOn f s) : MonotoneOn (fun x => -f x) s

ink

theorem AntitoneOn.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : Preorder β] {f : β → α} {s : Set β} (hf : AntitoneOn f s) : MonotoneOn (fun x => (f x)⁻¹) s

ink

theorem StrictMono.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : β → α} (hf : StrictMono f) : StrictAnti fun x => -f x

ink

theorem StrictMono.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : β → α} (hf : StrictMono f) : StrictAnti fun x => (f x)⁻¹

ink

theorem StrictAnti.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : β → α} (hf : StrictAnti f) : StrictMono fun x => -f x

ink

theorem StrictAnti.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : β → α} (hf : StrictAnti f) : StrictMono fun x => (f x)⁻¹

ink

theorem StrictMonoOn.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : β → α} {s : Set β} (hf : StrictMonoOn f s) : StrictAntiOn (fun x => -f x) s

ink

theorem StrictMonoOn.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : β → α} {s : Set β} (hf : StrictMonoOn f s) : StrictAntiOn (fun x => (f x)⁻¹) s

ink

theorem StrictAntiOn.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : β → α} {s : Set β} (hf : StrictAntiOn f s) : StrictMonoOn (fun x => -f x) s

ink

theorem StrictAntiOn.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : β → α} {s : Set β} (hf : StrictAntiOn f s) : StrictMonoOn (fun x => (f x)⁻¹) s