mathlib docs: algebra.ordered

A canonically ordered additive monoid is an ordered commutative additive monoid in which the ordering coincides with the divisibility relation, which is to say, a ≤ b iff there exists c with b = a + c. This is satisfied by the natural numbers, for example, but not the integers or other ordered groups.

Instances

source

@[instance]

def canonically_ordered_add_monoid.to_ordered_add_comm_monoid (α : Type u_1) [s : canonically_ordered_add_monoid α] :

ordered_add_comm_monoid α

source

theorem le_iff_exists_add {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :

a ≤ b ↔ ∃ (c : α), b = a + c

source

@[simp]

theorem zero_le {α : Type u} [canonically_ordered_add_monoid α] (a : α) :

0 ≤ a

source

@[simp]

theorem bot_eq_zero {α : Type u} [canonically_ordered_add_monoid α] :

⊥ = 0

source

@[simp]

theorem add_eq_zero_iff {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :

a + b = 0 ↔ a = 0 ∧ b = 0

source

@[simp]

theorem le_zero_iff_eq {α : Type u} [canonically_ordered_add_monoid α] {a : α} :

a ≤ 0 ↔ a = 0

source

theorem zero_lt_iff_ne_zero {α : Type u} [canonically_ordered_add_monoid α] {a : α} :

0 < a ↔ a ≠ 0

source

theorem exists_pos_add_of_lt {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :

a < b → (∃ (c : α) (H : c > 0), a + c = b)

source

theorem le_add_left {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} :

a ≤ c → a ≤ b + c

source

theorem le_add_right {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} :

a ≤ b → a ≤ b + c

source

@[instance]

def with_zero.canonically_ordered_add_monoid {α : Type u} [canonically_ordered_add_monoid α] :

canonically_ordered_add_monoid (with_zero α)

Equations

with_zero.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add (with_zero.ordered_add_comm_monoid zero_le), add_assoc := _, zero := ordered_add_comm_monoid.zero (with_zero.ordered_add_comm_monoid zero_le), zero_add := _, add_zero := _, add_comm := _, le := ordered_add_comm_monoid.le (with_zero.ordered_add_comm_monoid zero_le), lt := ordered_add_comm_monoid.lt (with_zero.ordered_add_comm_monoid zero_le), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := 0, bot_le := _, le_iff_exists_add := _}

source

@[instance]

def with_top.canonically_ordered_add_monoid {α : Type u} [canonically_ordered_add_monoid α] :

canonically_ordered_add_monoid (with_top α)

Equations

with_top.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add with_top.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero with_top.ordered_add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, le := order_bot.le with_top.order_bot, lt := order_bot.lt with_top.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := order_bot.bot with_top.order_bot, bot_le := _, le_iff_exists_add := _}

source

@[instance]

def canonically_linear_ordered_add_monoid.to_canonically_ordered_add_monoid (α : Type u_1) [s : canonically_linear_ordered_add_monoid α] :

canonically_ordered_add_monoid α

source

@[class]

structure canonically_linear_ordered_add_monoid :

Type u_1 → Type u_1

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
add_comm : ∀ (a b : α), a + b = b + a
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
le_iff_exists_add : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a + c_1
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt

A canonically linear-ordered additive monoid is a canonically ordered additive monoid whose ordering is a decidable linear order.

source

@[instance]

def canonically_linear_ordered_add_monoid.to_decidable_linear_order (α : Type u_1) [s : canonically_linear_ordered_add_monoid α] :

decidable_linear_order α

source

@[instance]

def canonically_linear_ordered_add_monoid.semilattice_sup_bot {α : Type u} [canonically_linear_ordered_add_monoid α] :

semilattice_sup_bot α

Equations

canonically_linear_ordered_add_monoid.semilattice_sup_bot = {bot := order_bot.bot (canonically_ordered_add_monoid.to_order_bot α), le := lattice.le lattice_of_decidable_linear_order, lt := lattice.lt lattice_of_decidable_linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := lattice.sup lattice_of_decidable_linear_order, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def ordered_cancel_add_comm_monoid.to_partial_order (α : Type u) [s : ordered_cancel_add_comm_monoid α] :

partial_order α

source

@[instance]

def ordered_cancel_add_comm_monoid.to_add_right_cancel_semigroup (α : Type u) [s : ordered_cancel_add_comm_monoid α] :

add_right_cancel_semigroup α

source

@[class]

structure ordered_cancel_add_comm_monoid :

Type u → Type u

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
add_comm : ∀ (a b : α), a + b = b + a
add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
add_right_cancel : ∀ (a b c_1 : α), a + b = c_1 + b → a = c_1
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
le_of_add_le_add_left : ∀ (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1

An ordered cancellative additive commutative monoid is an additive commutative monoid with a partial order, in which addition is cancellative and strictly monotone.

Instances

source

@[instance]

def ordered_cancel_add_comm_monoid.to_add_left_cancel_semigroup (α : Type u) [s : ordered_cancel_add_comm_monoid α] :

add_left_cancel_semigroup α

source

@[instance]

def ordered_cancel_add_comm_monoid.to_add_comm_monoid (α : Type u) [s : ordered_cancel_add_comm_monoid α] :

add_comm_monoid α

source

@[instance]

def ordered_cancel_comm_monoid.to_left_cancel_semigroup (α : Type u) [s : ordered_cancel_comm_monoid α] :

left_cancel_semigroup α

source

@[class]

structure ordered_cancel_comm_monoid :

Type u → Type u

mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), a * b * c_1 = a * (b * c_1)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
mul_comm : ∀ (a b : α), a * b = b * a
mul_left_cancel : ∀ (a b c_1 : α), a * b = a * c_1 → b = c_1
mul_right_cancel : ∀ (a b c_1 : α), a * b = c_1 * b → a = c_1
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
le_of_mul_le_mul_left : ∀ (a b c_1 : α), a * b ≤ a * c_1 → b ≤ c_1

An ordered cancellative commutative monoid is a commutative monoid with a partial order, in which multiplication is cancellative and strictly monotone.

Instances

source

@[instance]

def ordered_cancel_comm_monoid.to_comm_monoid (α : Type u) [s : ordered_cancel_comm_monoid α] :

comm_monoid α

source

@[instance]

def ordered_cancel_comm_monoid.to_right_cancel_semigroup (α : Type u) [s : ordered_cancel_comm_monoid α] :

right_cancel_semigroup α

source

@[instance]

def ordered_cancel_comm_monoid.to_partial_order (α : Type u) [s : ordered_cancel_comm_monoid α] :

partial_order α

source

@[instance]

def ordered_cancel_add_comm_monoid.to_left_cancel_add_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] :

add_left_cancel_monoid α

source

@[instance]

def ordered_cancel_comm_monoid.to_left_cancel_monoid {α : Type u} [ordered_cancel_comm_monoid α] :

left_cancel_monoid α

Equations

ordered_cancel_comm_monoid.to_left_cancel_monoid = {mul := ordered_cancel_comm_monoid.mul _inst_1, mul_assoc := _, mul_left_cancel := _, one := ordered_cancel_comm_monoid.one _inst_1, one_mul := _, mul_one := _}

source

theorem le_of_add_le_add_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

a + b ≤ a + c → b ≤ c

source

theorem le_of_mul_le_mul_left' {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

a * b ≤ a * c → b ≤ c

source

@[instance]

def ordered_cancel_comm_monoid.to_ordered_comm_monoid {α : Type u} [ordered_cancel_comm_monoid α] :

ordered_comm_monoid α

Equations

ordered_cancel_comm_monoid.to_ordered_comm_monoid = {mul := ordered_cancel_comm_monoid.mul _inst_1, mul_assoc := _, one := ordered_cancel_comm_monoid.one _inst_1, one_mul := _, mul_one := _, mul_comm := _, le := ordered_cancel_comm_monoid.le _inst_1, lt := ordered_cancel_comm_monoid.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}

source

@[instance]

def ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] :

ordered_add_comm_monoid α

source

theorem mul_lt_mul_left' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (h : a < b) (c : α) :

c * a < c * b

source

theorem add_lt_add_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (h : a < b) (c : α) :

c + a < c + b

source

theorem add_lt_add_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (h : a < b) (c : α) :

a + c < b + c

source

theorem mul_lt_mul_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (h : a < b) (c : α) :

a * c < b * c

source

theorem mul_lt_mul''' {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} :

a < b → c < d → a * c < b * d

source

theorem add_lt_add {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} :

a < b → c < d → a + c < b + d

source

theorem add_lt_add_of_le_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} :

a ≤ b → c < d → a + c < b + d

source

theorem mul_lt_mul_of_le_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} :

a ≤ b → c < d → a * c < b * d

source

theorem add_lt_add_of_lt_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} :

a < b → c ≤ d → a + c < b + d

source

theorem mul_lt_mul_of_lt_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} :

a < b → c ≤ d → a * c < b * d

source

theorem lt_add_of_pos_right {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

0 < b → a < a + b

source

theorem lt_mul_of_one_lt_right' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

1 < b → a < a * b

source

theorem lt_add_of_pos_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

0 < b → a < b + a

source

theorem lt_mul_of_one_lt_left' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

1 < b → a < b * a

source

theorem le_of_mul_le_mul_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

a * b ≤ c * b → a ≤ c

source

theorem le_of_add_le_add_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

a + b ≤ c + b → a ≤ c

source

theorem mul_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :

a < 1 → b < 1 → a * b < 1

source

theorem add_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a < 0 → b < 0 → a + b < 0

source

theorem mul_lt_one_of_lt_one_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :

a < 1 → b ≤ 1 → a * b < 1

source

theorem add_neg_of_neg_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a < 0 → b ≤ 0 → a + b < 0

source

theorem add_neg_of_nonpos_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a ≤ 0 → b < 0 → a + b < 0

source

theorem mul_lt_one_of_le_one_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :

a ≤ 1 → b < 1 → a * b < 1

source

theorem lt_add_of_pos_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

0 < a → b ≤ c → b < a + c

source

theorem lt_mul_of_one_lt_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

1 < a → b ≤ c → b < a * c

source

theorem lt_mul_of_le_of_one_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

b ≤ c → 1 < a → b < c * a

source

theorem lt_add_of_le_of_pos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

b ≤ c → 0 < a → b < c + a

source

theorem add_le_of_nonpos_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

a ≤ 0 → b ≤ c → a + b ≤ c

source

theorem mul_le_of_le_one_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

a ≤ 1 → b ≤ c → a * b ≤ c

source

theorem add_le_of_le_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

b ≤ c → a ≤ 0 → b + a ≤ c

source

theorem mul_le_of_le_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

b ≤ c → a ≤ 1 → b * a ≤ c

source

theorem mul_lt_of_lt_one_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

a < 1 → b ≤ c → a * b < c

source

theorem add_lt_of_neg_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

a < 0 → b ≤ c → a + b < c

source

theorem mul_lt_of_le_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

b ≤ c → a < 1 → b * a < c

source

theorem add_lt_of_le_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

b ≤ c → a < 0 → b + a < c

source

theorem lt_mul_of_one_le_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

1 ≤ a → b < c → b < a * c

source

theorem lt_add_of_nonneg_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

0 ≤ a → b < c → b < a + c

source

theorem lt_mul_of_lt_of_one_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

b < c → 1 ≤ a → b < c * a

source

theorem lt_add_of_lt_of_nonneg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

b < c → 0 ≤ a → b < c + a

source

theorem lt_mul_of_one_lt_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

1 < a → b < c → b < a * c

source

theorem lt_add_of_pos_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

0 < a → b < c → b < a + c

source

theorem lt_mul_of_lt_of_one_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

b < c → 1 < a → b < c * a

source

theorem lt_add_of_lt_of_pos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

b < c → 0 < a → b < c + a

source

theorem mul_lt_of_le_one_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

a ≤ 1 → b < c → a * b < c

source

theorem add_lt_of_nonpos_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

a ≤ 0 → b < c → a + b < c

source

theorem add_lt_of_lt_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

b < c → a ≤ 0 → b + a < c

source

theorem mul_lt_of_lt_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

b < c → a ≤ 1 → b * a < c

source

theorem add_lt_of_neg_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

a < 0 → b < c → a + b < c

source

theorem mul_lt_of_lt_one_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

a < 1 → b < c → a * b < c

source

theorem add_lt_of_lt_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

b < c → a < 0 → b + a < c

source

theorem mul_lt_of_lt_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

b < c → a < 1 → b * a < c

source

@[simp]

theorem add_le_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b c : α} :

a + b ≤ a + c ↔ b ≤ c

source

@[simp]

theorem mul_le_mul_iff_left {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b c : α} :

a * b ≤ a * c ↔ b ≤ c

source

@[simp]

theorem add_le_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (c : α) :

a + c ≤ b + c ↔ a ≤ b

source

@[simp]

theorem mul_le_mul_iff_right {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (c : α) :

a * c ≤ b * c ↔ a ≤ b

source

@[simp]

theorem add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b c : α} :

a + b < a + c ↔ b < c

source

@[simp]

theorem mul_lt_mul_iff_left {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b c : α} :

a * b < a * c ↔ b < c

source

@[simp]

theorem add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (c : α) :

a + c < b + c ↔ a < b

source

@[simp]

theorem mul_lt_mul_iff_right {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (c : α) :

a * c < b * c ↔ a < b

source

@[simp]

theorem le_mul_iff_one_le_right' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

a ≤ a * b ↔ 1 ≤ b

source

@[simp]

theorem le_add_iff_nonneg_right {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

a ≤ a + b ↔ 0 ≤ b

source

@[simp]

theorem le_mul_iff_one_le_left' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

a ≤ b * a ↔ 1 ≤ b

source

@[simp]

theorem le_add_iff_nonneg_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

a ≤ b + a ↔ 0 ≤ b

source

@[simp]

theorem lt_add_iff_pos_right {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

a < a + b ↔ 0 < b

source

@[simp]

theorem lt_mul_iff_one_lt_right' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

a < a * b ↔ 1 < b

source

@[simp]

theorem lt_mul_iff_one_lt_left' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

a < b * a ↔ 1 < b

source

@[simp]

theorem lt_add_iff_pos_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

a < b + a ↔ 0 < b

source

@[simp]

theorem add_le_iff_nonpos_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a + b ≤ b ↔ a ≤ 0

source

@[simp]

theorem mul_le_iff_le_one_left' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :

a * b ≤ b ↔ a ≤ 1

source

@[simp]

theorem add_le_iff_nonpos_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a + b ≤ a ↔ b ≤ 0

source

@[simp]

theorem mul_le_iff_le_one_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :

a * b ≤ a ↔ b ≤ 1

source

@[simp]

theorem add_lt_iff_neg_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a + b < b ↔ a < 0

source

@[simp]

theorem mul_lt_iff_lt_one_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :

a * b < b ↔ a < 1

source

@[simp]

theorem mul_lt_iff_lt_one_left' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :

a * b < a ↔ b < 1

source

@[simp]

theorem add_lt_iff_neg_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a + b < a ↔ b < 0

source

theorem add_eq_zero_iff_eq_zero_of_nonneg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

0 ≤ a → 0 ≤ b → (a + b = 0 ↔ a = 0 ∧ b = 0)

source

theorem mul_eq_one_iff_eq_one_of_one_le {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :

1 ≤ a → 1 ≤ b → (a * b = 1 ↔ a = 1 ∧ b = 1)

source

theorem monotone.add_strict_mono {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} :

monotone f → strict_mono g → strict_mono (λ (x : β), f x + g x)

source

theorem monotone.mul_strict_mono' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} :

monotone f → strict_mono g → strict_mono (λ (x : β), f x * g x)

source

theorem strict_mono.mul_monotone' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} :

strict_mono f → monotone g → strict_mono (λ (x : β), f x * g x)

source

theorem strict_mono.add_monotone {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} :

strict_mono f → monotone g → strict_mono (λ (x : β), f x + g x)

source

theorem strict_mono.add_const {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :

strict_mono (λ (x : β), f x + c)

source

theorem strict_mono.mul_const' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :

strict_mono (λ (x : β), f x * c)

source

theorem strict_mono.const_mul' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :

strict_mono (λ (x : β), c * f x)

source

theorem strict_mono.const_add {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :

strict_mono (λ (x : β), c + f x)

source

theorem with_top.add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_top α} :

a < ⊤ → (a + c < a + b ↔ c < b)

source

theorem with_top.add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_top α} :

a < ⊤ → (c + a < b + a ↔ c < b)

source

@[instance]

def ordered_add_comm_group.to_add_comm_group (α : Type u) [s : ordered_add_comm_group α] :

add_comm_group α

source

@[class]

structure ordered_add_comm_group :

Type u → Type u

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
neg : α → α
add_left_neg : ∀ (a : α), -a + a = 0
add_comm : ∀ (a b : α), a + b = b + a
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b

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

Instances

source

@[instance]

def ordered_add_comm_group.to_partial_order (α : Type u) [s : ordered_add_comm_group α] :

partial_order α

source

@[class]

structure ordered_comm_group :

Type u → Type u

mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), a * b * c_1 = a * (b * c_1)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
inv : α → α
mul_left_inv : ∀ (a : α), a⁻¹ * a = 1
mul_comm : ∀ (a b : α), a * b = b * a
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b

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

Instances

source

@[instance]

def ordered_comm_group.to_partial_order (α : Type u) [s : ordered_comm_group α] :

partial_order α

source

@[instance]

def ordered_comm_group.to_comm_group (α : Type u) [s : ordered_comm_group α] :

comm_group α

source

@[instance]

def add_units.ordered_add_comm_group {α : Type u} [ordered_add_comm_monoid α] :

ordered_add_comm_group (add_units α)

source

@[instance]

def units.ordered_comm_group {α : Type u} [ordered_comm_monoid α] :

ordered_comm_group (units α)

The units of an ordered commutative monoid form an ordered commutative group.

Equations

units.ordered_comm_group = {mul := comm_group.mul infer_instance, mul_assoc := _, one := comm_group.one infer_instance, one_mul := _, mul_one := _, inv := comm_group.inv infer_instance, mul_left_inv := _, mul_comm := _, le := partial_order.le units.partial_order, lt := partial_order.lt units.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}

source

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

c + a < c + b

source

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

c * a < c * b

source

theorem ordered_comm_group.le_of_mul_le_mul_left {α : Type u} [ordered_comm_group α] {a b c : α} :

a * b ≤ a * c → b ≤ c

source

theorem ordered_add_comm_group.le_of_add_le_add_left {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a + b ≤ a + c → b ≤ c

source

theorem ordered_comm_group.lt_of_mul_lt_mul_left {α : Type u} [ordered_comm_group α] {a b c : α} :

a * b < a * c → b < c

source

theorem ordered_add_comm_group.lt_of_add_lt_add_left {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a + b < a + c → b < c

source

@[instance]

def ordered_add_comm_group.to_ordered_cancel_add_comm_monoid (α : Type u) [s : ordered_add_comm_group α] :

ordered_cancel_add_comm_monoid α

source

@[instance]

def ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u) [s : ordered_comm_group α] :

ordered_cancel_comm_monoid α

Equations

ordered_comm_group.to_ordered_cancel_comm_monoid α = {mul := ordered_comm_group.mul s, mul_assoc := _, one := ordered_comm_group.one s, one_mul := _, mul_one := _, mul_comm := _, mul_left_cancel := _, mul_right_cancel := _, le := ordered_comm_group.le s, lt := ordered_comm_group.lt s, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}

source

theorem neg_le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :

a ≤ b → -b ≤ -a

source

theorem inv_le_inv' {α : Type u} [ordered_comm_group α] {a b : α} :

a ≤ b → b⁻¹ ≤ a⁻¹

source

theorem le_of_inv_le_inv {α : Type u} [ordered_comm_group α] {a b : α} :

b⁻¹ ≤ a⁻¹ → a ≤ b

source

theorem le_of_neg_le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :

-b ≤ -a → a ≤ b

source

theorem one_le_of_inv_le_one {α : Type u} [ordered_comm_group α] {a : α} :

a⁻¹ ≤ 1 → 1 ≤ a

source

theorem nonneg_of_neg_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} :

-a ≤ 0 → 0 ≤ a

source

theorem inv_le_one_of_one_le {α : Type u} [ordered_comm_group α] {a : α} :

1 ≤ a → a⁻¹ ≤ 1

source

theorem neg_nonpos_of_nonneg {α : Type u} [ordered_add_comm_group α] {a : α} :

0 ≤ a → -a ≤ 0

source

theorem le_one_of_one_le_inv {α : Type u} [ordered_comm_group α] {a : α} :

1 ≤ a⁻¹ → a ≤ 1

source

theorem nonpos_of_neg_nonneg {α : Type u} [ordered_add_comm_group α] {a : α} :

0 ≤ -a → a ≤ 0

source

theorem neg_nonneg_of_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} :

a ≤ 0 → 0 ≤ -a

source

theorem one_le_inv_of_le_one {α : Type u} [ordered_comm_group α] {a : α} :

a ≤ 1 → 1 ≤ a⁻¹

source

theorem inv_lt_inv' {α : Type u} [ordered_comm_group α] {a b : α} :

a < b → b⁻¹ < a⁻¹

source

theorem neg_lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :

a < b → -b < -a

source

theorem lt_of_neg_lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :

-b < -a → a < b

source

theorem lt_of_inv_lt_inv {α : Type u} [ordered_comm_group α] {a b : α} :

b⁻¹ < a⁻¹ → a < b

source

theorem one_lt_of_inv_inv {α : Type u} [ordered_comm_group α] {a : α} :

a⁻¹ < 1 → 1 < a

source

theorem pos_of_neg_neg {α : Type u} [ordered_add_comm_group α] {a : α} :

-a < 0 → 0 < a

source

theorem inv_inv_of_one_lt {α : Type u} [ordered_comm_group α] {a : α} :

1 < a → a⁻¹ < 1

source

theorem neg_neg_of_pos {α : Type u} [ordered_add_comm_group α] {a : α} :

0 < a → -a < 0

source

theorem inv_of_one_lt_inv {α : Type u} [ordered_comm_group α] {a : α} :

1 < a⁻¹ → a < 1

source

theorem neg_of_neg_pos {α : Type u} [ordered_add_comm_group α] {a : α} :

0 < -a → a < 0

source

theorem neg_pos_of_neg {α : Type u} [ordered_add_comm_group α] {a : α} :

a < 0 → 0 < -a

source

theorem one_lt_inv_of_inv {α : Type u} [ordered_comm_group α] {a : α} :

a < 1 → 1 < a⁻¹

source

theorem le_inv_of_le_inv {α : Type u} [ordered_comm_group α] {a b : α} :

a ≤ b⁻¹ → b ≤ a⁻¹

source

theorem le_neg_of_le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :

a ≤ -b → b ≤ -a

source

theorem inv_le_of_inv_le {α : Type u} [ordered_comm_group α] {a b : α} :

a⁻¹ ≤ b → b⁻¹ ≤ a

source

theorem neg_le_of_neg_le {α : Type u} [ordered_add_comm_group α] {a b : α} :

-a ≤ b → -b ≤ a

source

theorem lt_inv_of_lt_inv {α : Type u} [ordered_comm_group α] {a b : α} :

a < b⁻¹ → b < a⁻¹

source

theorem lt_neg_of_lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :

a < -b → b < -a

source

theorem neg_lt_of_neg_lt {α : Type u} [ordered_add_comm_group α] {a b : α} :

-a < b → -b < a

source

theorem inv_lt_of_inv_lt {α : Type u} [ordered_comm_group α] {a b : α} :

a⁻¹ < b → b⁻¹ < a

source

theorem mul_le_of_le_inv_mul {α : Type u} [ordered_comm_group α] {a b c : α} :

b ≤ a⁻¹ * c → a * b ≤ c

source

theorem add_le_of_le_neg_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

b ≤ -a + c → a + b ≤ c

source

theorem le_neg_add_of_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a + b ≤ c → b ≤ -a + c

source

theorem le_inv_mul_of_mul_le {α : Type u} [ordered_comm_group α] {a b c : α} :

a * b ≤ c → b ≤ a⁻¹ * c

source

theorem le_mul_of_inv_mul_le {α : Type u} [ordered_comm_group α] {a b c : α} :

b⁻¹ * a ≤ c → a ≤ b * c

source

theorem le_add_of_neg_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-b + a ≤ c → a ≤ b + c

source

theorem neg_add_le_of_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a ≤ b + c → -b + a ≤ c

source

theorem inv_mul_le_of_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} :

a ≤ b * c → b⁻¹ * a ≤ c

source

theorem le_add_of_neg_add_le_left {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-b + a ≤ c → a ≤ b + c

source

theorem le_mul_of_inv_mul_le_left {α : Type u} [ordered_comm_group α] {a b c : α} :

b⁻¹ * a ≤ c → a ≤ b * c

source

theorem inv_mul_le_left_of_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} :

a ≤ b * c → b⁻¹ * a ≤ c

source

theorem neg_add_le_left_of_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a ≤ b + c → -b + a ≤ c

source

theorem le_mul_of_inv_mul_le_right {α : Type u} [ordered_comm_group α] {a b c : α} :

c⁻¹ * a ≤ b → a ≤ b * c

source

theorem le_add_of_neg_add_le_right {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-c + a ≤ b → a ≤ b + c

source

theorem inv_mul_le_right_of_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} :

a ≤ b * c → c⁻¹ * a ≤ b

source

theorem neg_add_le_right_of_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a ≤ b + c → -c + a ≤ b

source

theorem add_lt_of_lt_neg_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

b < -a + c → a + b < c

source

theorem mul_lt_of_lt_inv_mul {α : Type u} [ordered_comm_group α] {a b c : α} :

b < a⁻¹ * c → a * b < c

source

theorem lt_neg_add_of_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a + b < c → b < -a + c

source

theorem lt_inv_mul_of_mul_lt {α : Type u} [ordered_comm_group α] {a b c : α} :

a * b < c → b < a⁻¹ * c

source

theorem lt_add_of_neg_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-b + a < c → a < b + c

source

theorem lt_mul_of_inv_mul_lt {α : Type u} [ordered_comm_group α] {a b c : α} :

b⁻¹ * a < c → a < b * c

source

theorem neg_add_lt_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a < b + c → -b + a < c

source

theorem inv_mul_lt_of_lt_mul {α : Type u} [ordered_comm_group α] {a b c : α} :

a < b * c → b⁻¹ * a < c

source

theorem lt_mul_of_inv_mul_lt_left {α : Type u} [ordered_comm_group α] {a b c : α} :

b⁻¹ * a < c → a < b * c

source

theorem lt_add_of_neg_add_lt_left {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-b + a < c → a < b + c

source

theorem neg_add_lt_left_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a < b + c → -b + a < c

source

theorem inv_mul_lt_left_of_lt_mul {α : Type u} [ordered_comm_group α] {a b c : α} :

a < b * c → b⁻¹ * a < c

source

theorem lt_mul_of_inv_mul_lt_right {α : Type u} [ordered_comm_group α] {a b c : α} :

c⁻¹ * a < b → a < b * c

source

theorem lt_add_of_neg_add_lt_right {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-c + a < b → a < b + c

source

theorem neg_add_lt_right_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a < b + c → -c + a < b

source

theorem inv_mul_lt_right_of_lt_mul {α : Type u} [ordered_comm_group α] {a b c : α} :

a < b * c → c⁻¹ * a < b

source

@[simp]

theorem inv_lt_one_iff_one_lt {α : Type u} [ordered_comm_group α] {a : α} :

a⁻¹ < 1 ↔ 1 < a

source

@[simp]

theorem neg_neg_iff_pos {α : Type u} [ordered_add_comm_group α] {a : α} :

-a < 0 ↔ 0 < a

source

@[simp]

theorem neg_le_neg_iff {α : Type u} [ordered_add_comm_group α] {a b : α} :

-a ≤ -b ↔ b ≤ a

source

@[simp]

theorem inv_le_inv_iff {α : Type u} [ordered_comm_group α] {a b : α} :

a⁻¹ ≤ b⁻¹ ↔ b ≤ a

source

theorem neg_le {α : Type u} [ordered_add_comm_group α] {a b : α} :

-a ≤ b ↔ -b ≤ a

source

theorem inv_le' {α : Type u} [ordered_comm_group α] {a b : α} :

a⁻¹ ≤ b ↔ b⁻¹ ≤ a

source

theorem le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :

a ≤ -b ↔ b ≤ -a

source

theorem le_inv' {α : Type u} [ordered_comm_group α] {a b : α} :

a ≤ b⁻¹ ↔ b ≤ a⁻¹

source

theorem inv_le_iff_one_le_mul {α : Type u} [ordered_comm_group α] {a b : α} :

a⁻¹ ≤ b ↔ 1 ≤ a * b

source

theorem neg_le_iff_add_nonneg {α : Type u} [ordered_add_comm_group α] {a b : α} :

-a ≤ b ↔ 0 ≤ a + b

source

theorem le_neg_iff_add_nonpos {α : Type u} [ordered_add_comm_group α] {a b : α} :

a ≤ -b ↔ a + b ≤ 0

source

theorem le_inv_iff_mul_le_one {α : Type u} [ordered_comm_group α] {a b : α} :

a ≤ b⁻¹ ↔ a * b ≤ 1

source

@[simp]

theorem inv_le_one' {α : Type u} [ordered_comm_group α] {a : α} :

a⁻¹ ≤ 1 ↔ 1 ≤ a

source

@[simp]

theorem neg_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} :

-a ≤ 0 ↔ 0 ≤ a

source

@[simp]

theorem one_le_inv' {α : Type u} [ordered_comm_group α] {a : α} :

1 ≤ a⁻¹ ↔ a ≤ 1

source

@[simp]

theorem neg_nonneg {α : Type u} [ordered_add_comm_group α] {a : α} :

0 ≤ -a ↔ a ≤ 0

source

theorem neg_le_self {α : Type u} [ordered_add_comm_group α] {a : α} :

0 ≤ a → -a ≤ a

source

theorem inv_le_self {α : Type u} [ordered_comm_group α] {a : α} :

1 ≤ a → a⁻¹ ≤ a

source

theorem self_le_neg {α : Type u} [ordered_add_comm_group α] {a : α} :

a ≤ 0 → a ≤ -a

source

theorem self_le_inv {α : Type u} [ordered_comm_group α] {a : α} :

a ≤ 1 → a ≤ a⁻¹

source

@[simp]

theorem inv_lt_inv_iff {α : Type u} [ordered_comm_group α] {a b : α} :

a⁻¹ < b⁻¹ ↔ b < a

source

@[simp]

theorem neg_lt_neg_iff {α : Type u} [ordered_add_comm_group α] {a b : α} :

-a < -b ↔ b < a

source

theorem neg_lt_zero {α : Type u} [ordered_add_comm_group α] {a : α} :

-a < 0 ↔ 0 < a

source

theorem inv_lt_one' {α : Type u} [ordered_comm_group α] {a : α} :

a⁻¹ < 1 ↔ 1 < a

source

theorem neg_pos {α : Type u} [ordered_add_comm_group α] {a : α} :

0 < -a ↔ a < 0

source

theorem one_lt_inv' {α : Type u} [ordered_comm_group α] {a : α} :

1 < a⁻¹ ↔ a < 1

source

theorem neg_lt {α : Type u} [ordered_add_comm_group α] {a b : α} :

-a < b ↔ -b < a

source

theorem inv_lt' {α : Type u} [ordered_comm_group α] {a b : α} :

a⁻¹ < b ↔ b⁻¹ < a

source

theorem lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :

a < -b ↔ b < -a

source

theorem lt_inv' {α : Type u} [ordered_comm_group α] {a b : α} :

a < b⁻¹ ↔ b < a⁻¹

source

theorem le_inv_mul_iff_mul_le {α : Type u} [ordered_comm_group α] {a b c : α} :

b ≤ a⁻¹ * c ↔ a * b ≤ c

source

theorem le_neg_add_iff_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :

b ≤ -a + c ↔ a + b ≤ c

source

@[simp]

theorem inv_mul_le_iff_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} :

b⁻¹ * a ≤ c ↔ a ≤ b * c

source

@[simp]

theorem neg_add_le_iff_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-b + a ≤ c ↔ a ≤ b + c

source

theorem add_neg_le_iff_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a + -c ≤ b ↔ a ≤ b + c

source

theorem mul_inv_le_iff_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} :

a * c⁻¹ ≤ b ↔ a ≤ b * c

source

@[simp]

theorem mul_inv_le_iff_le_mul' {α : Type u} [ordered_comm_group α] {a b c : α} :

a * b⁻¹ ≤ c ↔ a ≤ b * c

source

@[simp]

theorem add_neg_le_iff_le_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a + -b ≤ c ↔ a ≤ b + c

source

theorem neg_add_le_iff_le_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-c + a ≤ b ↔ a ≤ b + c

source

theorem inv_mul_le_iff_le_mul' {α : Type u} [ordered_comm_group α] {a b c : α} :

c⁻¹ * a ≤ b ↔ a ≤ b * c

source

@[simp]

theorem lt_neg_add_iff_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :

b < -a + c ↔ a + b < c

source

@[simp]

theorem lt_inv_mul_iff_mul_lt {α : Type u} [ordered_comm_group α] {a b c : α} :

b < a⁻¹ * c ↔ a * b < c

source

@[simp]

theorem inv_mul_lt_iff_lt_mul {α : Type u} [ordered_comm_group α] {a b c : α} :

b⁻¹ * a < c ↔ a < b * c

source

@[simp]

theorem neg_add_lt_iff_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-b + a < c ↔ a < b + c

source

theorem neg_add_lt_iff_lt_add_right {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-c + a < b ↔ a < b + c

source

theorem inv_mul_lt_iff_lt_mul_right {α : Type u} [ordered_comm_group α] {a b c : α} :

c⁻¹ * a < b ↔ a < b * c

source

theorem sub_le_sub_iff {α : Type u} [ordered_add_comm_group α] (a b c d : α) :

a + -b ≤ c + -d ↔ a + d ≤ c + b

source

theorem div_le_div_iff' {α : Type u} [ordered_comm_group α] (a b c d : α) :

a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b

source

theorem sub_nonneg_of_le {α : Type u} [ordered_add_comm_group α] {a b : α} :

b ≤ a → 0 ≤ a - b

source

theorem le_of_sub_nonneg {α : Type u} [ordered_add_comm_group α] {a b : α} :

0 ≤ a - b → b ≤ a

source

theorem sub_nonpos_of_le {α : Type u} [ordered_add_comm_group α] {a b : α} :

a ≤ b → a - b ≤ 0

source

theorem le_of_sub_nonpos {α : Type u} [ordered_add_comm_group α] {a b : α} :

a - b ≤ 0 → a ≤ b

source

theorem sub_pos_of_lt {α : Type u} [ordered_add_comm_group α] {a b : α} :

b < a → 0 < a - b

source

theorem lt_of_sub_pos {α : Type u} [ordered_add_comm_group α] {a b : α} :

0 < a - b → b < a

source

theorem sub_neg_of_lt {α : Type u} [ordered_add_comm_group α] {a b : α} :

a < b → a - b < 0

source

theorem lt_of_sub_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :

a - b < 0 → a < b

source

theorem add_le_of_le_sub_left {α : Type u} [ordered_add_comm_group α] {a b c : α} :

b ≤ c - a → a + b ≤ c

source

theorem le_sub_left_of_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a + b ≤ c → b ≤ c - a

source

theorem add_le_of_le_sub_right {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a ≤ c - b → a + b ≤ c

source

theorem le_sub_right_of_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a + b ≤ c → a ≤ c - b

source

theorem le_add_of_sub_left_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a - b ≤ c → a ≤ b + c

source

theorem sub_left_le_of_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a ≤ b + c → a - b ≤ c

source

theorem le_add_of_sub_right_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a - c ≤ b → a ≤ b + c

source

theorem sub_right_le_of_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a ≤ b + c → a - c ≤ b

source

theorem le_add_of_neg_le_sub_left {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-a ≤ b - c → c ≤ a + b

source

theorem neg_le_sub_left_of_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

c ≤ a + b → -a ≤ b - c

source

theorem le_add_of_neg_le_sub_right {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-b ≤ a - c → c ≤ a + b

source

theorem neg_le_sub_right_of_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

c ≤ a + b → -b ≤ a - c

source

theorem sub_le_of_sub_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a - b ≤ c → a - c ≤ b

source

theorem sub_le_sub_left {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a ≤ b) (c : α) :

c - b ≤ c - a

source

theorem sub_le_sub_right {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a ≤ b) (c : α) :

a - c ≤ b - c

source

theorem sub_le_sub {α : Type u} [ordered_add_comm_group α] {a b c d : α} :

a ≤ b → c ≤ d → a - d ≤ b - c

source

theorem add_lt_of_lt_sub_left {α : Type u} [ordered_add_comm_group α] {a b c : α} :

b < c - a → a + b < c

source

theorem lt_sub_left_of_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a + b < c → b < c - a

source

theorem add_lt_of_lt_sub_right {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a < c - b → a + b < c

source

theorem lt_sub_right_of_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a + b < c → a < c - b

source

theorem lt_add_of_sub_left_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a - b < c → a < b + c

source

theorem sub_left_lt_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a < b + c → a - b < c

source

theorem lt_add_of_sub_right_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a - c < b → a < b + c

source

theorem sub_right_lt_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a < b + c → a - c < b

source

theorem lt_add_of_neg_lt_sub_left {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-a < b - c → c < a + b

source

theorem neg_lt_sub_left_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

c < a + b → -a < b - c

source

theorem lt_add_of_neg_lt_sub_right {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-b < a - c → c < a + b

source

theorem neg_lt_sub_right_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

c < a + b → -b < a - c

source

theorem sub_lt_of_sub_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a - b < c → a - c < b

source

theorem sub_lt_sub_left {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a < b) (c : α) :

c - b < c - a

source

theorem sub_lt_sub_right {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a < b) (c : α) :

a - c < b - c

source

theorem sub_lt_sub {α : Type u} [ordered_add_comm_group α] {a b c d : α} :

a < b → c < d → a - d < b - c

source

theorem sub_lt_sub_of_le_of_lt {α : Type u} [ordered_add_comm_group α] {a b c d : α} :

a ≤ b → c < d → a - d < b - c

source

theorem sub_lt_sub_of_lt_of_le {α : Type u} [ordered_add_comm_group α] {a b c d : α} :

a < b → c ≤ d → a - d < b - c

source

theorem sub_le_self {α : Type u} [ordered_add_comm_group α] (a : α) {b : α} :

0 ≤ b → a - b ≤ a

source

theorem sub_lt_self {α : Type u} [ordered_add_comm_group α] (a : α) {b : α} :

0 < b → a - b < a

source

@[simp]

theorem sub_le_sub_iff_left {α : Type u} [ordered_add_comm_group α] (a : α) {b c : α} :

a - b ≤ a - c ↔ c ≤ b

source

@[simp]

theorem sub_le_sub_iff_right {α : Type u} [ordered_add_comm_group α] {a b : α} (c : α) :

a - c ≤ b - c ↔ a ≤ b

source

@[simp]

theorem sub_lt_sub_iff_left {α : Type u} [ordered_add_comm_group α] (a : α) {b c : α} :

a - b < a - c ↔ c < b

source

@[simp]

theorem sub_lt_sub_iff_right {α : Type u} [ordered_add_comm_group α] {a b : α} (c : α) :

a - c < b - c ↔ a < b

source

@[simp]

theorem sub_nonneg {α : Type u} [ordered_add_comm_group α] {a b : α} :

0 ≤ a - b ↔ b ≤ a

source

@[simp]

theorem sub_nonpos {α : Type u} [ordered_add_comm_group α] {a b : α} :

a - b ≤ 0 ↔ a ≤ b

source

@[simp]

theorem sub_pos {α : Type u} [ordered_add_comm_group α] {a b : α} :

0 < a - b ↔ b < a

source

@[simp]

theorem sub_lt_zero {α : Type u} [ordered_add_comm_group α] {a b : α} :

a - b < 0 ↔ a < b

source

theorem le_sub_iff_add_le' {α : Type u} [ordered_add_comm_group α] {a b c : α} :

b ≤ c - a ↔ a + b ≤ c

source

theorem le_sub_iff_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a ≤ c - b ↔ a + b ≤ c

source

theorem sub_le_iff_le_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a - b ≤ c ↔ a ≤ b + c

source

theorem sub_le_iff_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a - c ≤ b ↔ a ≤ b + c

source

@[simp]

theorem neg_le_sub_iff_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-b ≤ a - c ↔ c ≤ a + b

source

theorem neg_le_sub_iff_le_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-a ≤ b - c ↔ c ≤ a + b

source

theorem sub_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a - b ≤ c ↔ a - c ≤ b

source

theorem le_sub {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a ≤ b - c ↔ c ≤ b - a

source

theorem lt_sub_iff_add_lt' {α : Type u} [ordered_add_comm_group α] {a b c : α} :

b < c - a ↔ a + b < c

source

theorem lt_sub_iff_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a < c - b ↔ a + b < c

source

theorem sub_lt_iff_lt_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a - b < c ↔ a < b + c

source

theorem sub_lt_iff_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a - c < b ↔ a < b + c

source

@[simp]

theorem neg_lt_sub_iff_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-b < a - c ↔ c < a + b

source

theorem neg_lt_sub_iff_lt_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :

-a < b - c ↔ c < a + b

source

theorem sub_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a - b < c ↔ a - c < b

source

theorem lt_sub {α : Type u} [ordered_add_comm_group α] {a b c : α} :

a < b - c ↔ c < b - a

source

theorem sub_le_self_iff {α : Type u} [ordered_add_comm_group α] (a : α) {b : α} :

a - b ≤ a ↔ 0 ≤ b

source

theorem sub_lt_self_iff {α : Type u} [ordered_add_comm_group α] (a : α) {b : α} :

a - b < a ↔ 0 < b

source

def ordered_comm_group.mk' {α : Type u} [comm_group α] [partial_order α] :

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

Alternative constructor for ordered commutative groups, that avoids the field mul_lt_mul_left.

Equations

ordered_comm_group.mk' mul_le_mul_left = {mul := comm_group.mul _inst_1, mul_assoc := _, one := comm_group.one _inst_1, one_mul := _, mul_one := _, inv := comm_group.inv _inst_1, mul_left_inv := _, mul_comm := _, le := partial_order.le _inst_2, lt := partial_order.lt _inst_2, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := mul_le_mul_left}

source

def ordered_add_comm_group.mk' {α : Type u} [add_comm_group α] [partial_order α] :

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

Alternative constructor for ordered commutative groups, that avoids the field mul_lt_mul_left.

source

@[class]

structure decidable_linear_ordered_cancel_add_comm_monoid :

Type u → Type u

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
add_comm : ∀ (a b : α), a + b = b + a
add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
add_right_cancel : ∀ (a b c_1 : α), a + b = c_1 + b → a = c_1
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
le_of_add_le_add_left : ∀ (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt

A decidable linearly ordered cancellative additive commutative monoid is an additive commutative monoid with a decidable linear order in which addition is cancellative and strictly monotone.

Instances

source

@[instance]

def decidable_linear_ordered_cancel_add_comm_monoid.to_decidable_linear_order (α : Type u) [s : decidable_linear_ordered_cancel_add_comm_monoid α] :

decidable_linear_order α

source

@[instance]

def decidable_linear_ordered_cancel_add_comm_monoid.to_ordered_cancel_add_comm_monoid (α : Type u) [s : decidable_linear_ordered_cancel_add_comm_monoid α] :

ordered_cancel_add_comm_monoid α

source

theorem min_add_add_left {α : Type u} [decidable_linear_ordered_cancel_add_comm_monoid α] (a b c : α) :

min (a + b) (a + c) = a + min b c

source

theorem min_add_add_right {α : Type u} [decidable_linear_ordered_cancel_add_comm_monoid α] (a b c : α) :

min (a + c) (b + c) = min a b + c

source

theorem max_add_add_left {α : Type u} [decidable_linear_ordered_cancel_add_comm_monoid α] (a b c : α) :

max (a + b) (a + c) = a + max b c

source

theorem max_add_add_right {α : Type u} [decidable_linear_ordered_cancel_add_comm_monoid α] (a b c : α) :

max (a + c) (b + c) = max a b + c

source

@[instance]

def decidable_linear_ordered_add_comm_group.to_add_comm_group (α : Type u) [s : decidable_linear_ordered_add_comm_group α] :

add_comm_group α

source

@[class]

structure decidable_linear_ordered_add_comm_group :

Type u → Type u

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
neg : α → α
add_left_neg : ∀ (a : α), -a + a = 0
add_comm : ∀ (a b : α), a + b = b + a
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b

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

Instances

source

@[instance]

def decidable_linear_ordered_add_comm_group.to_decidable_linear_order (α : Type u) [s : decidable_linear_ordered_add_comm_group α] :

decidable_linear_order α

source

@[instance]

def decidable_linear_ordered_comm_group.to_ordered_add_comm_group (α : Type u) [s : decidable_linear_ordered_add_comm_group α] :

ordered_add_comm_group α

Equations

decidable_linear_ordered_comm_group.to_ordered_add_comm_group α = {add := decidable_linear_ordered_add_comm_group.add s, add_assoc := _, zero := decidable_linear_ordered_add_comm_group.zero s, zero_add := _, add_zero := _, neg := decidable_linear_ordered_add_comm_group.neg s, add_left_neg := _, add_comm := _, le := decidable_linear_ordered_add_comm_group.le s, lt := decidable_linear_ordered_add_comm_group.lt s, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}

source

@[instance]

def decidable_linear_ordered_add_comm_group.to_decidable_linear_ordered_cancel_add_comm_monoid {α : Type u} [decidable_linear_ordered_add_comm_group α] :

decidable_linear_ordered_cancel_add_comm_monoid α

Equations

decidable_linear_ordered_add_comm_group.to_decidable_linear_ordered_cancel_add_comm_monoid = {add := decidable_linear_ordered_add_comm_group.add _inst_1, add_assoc := _, zero := decidable_linear_ordered_add_comm_group.zero _inst_1, zero_add := _, add_zero := _, add_comm := _, add_left_cancel := _, add_right_cancel := _, le := decidable_linear_ordered_add_comm_group.le _inst_1, lt := decidable_linear_ordered_add_comm_group.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, le_total := _, decidable_le := decidable_linear_ordered_add_comm_group.decidable_le _inst_1, decidable_eq := decidable_linear_ordered_add_comm_group.decidable_eq _inst_1, decidable_lt := decidable_linear_ordered_add_comm_group.decidable_lt _inst_1}

source

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

c + a < c + b

source

theorem max_neg_neg {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :

max (-a) (-b) = -min a b

source

theorem min_eq_neg_max_neg_neg {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :

min a b = -max (-a) (-b)

source

theorem min_neg_neg {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :

min (-a) (-b) = -max a b

source

theorem max_eq_neg_min_neg_neg {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :

max a b = -min (-a) (-b)

source

def abs {α : Type u} [decidable_linear_ordered_add_comm_group α] :

α → α

abs a is the absolute value of a.

Equations

abs a = max a (-a)

source

theorem abs_of_nonneg {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} :

0 ≤ a → abs a = a

source

theorem abs_of_pos {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} :

0 < a → abs a = a

source

theorem abs_of_nonpos {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} :

a ≤ 0 → abs a = -a

source

theorem abs_of_neg {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} :

a < 0 → abs a = -a

source

@[simp]

theorem abs_zero {α : Type u} [decidable_linear_ordered_add_comm_group α] :

abs 0 = 0

source

@[simp]

theorem abs_neg {α : Type u} [decidable_linear_ordered_add_comm_group α] (a : α) :

abs (-a) = abs a

source

theorem abs_pos_of_pos {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} :

0 < a → 0 < abs a

source

theorem abs_pos_of_neg {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} :

a < 0 → 0 < abs a

source

theorem abs_sub {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :

abs (a - b) = abs (b - a)

source

theorem ne_zero_of_abs_ne_zero {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} :

abs a ≠ 0 → a ≠ 0

source

theorem eq_zero_of_neg_eq {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} :

-a = a → a = 0

source

theorem abs_nonneg {α : Type u} [decidable_linear_ordered_add_comm_group α] (a : α) :

0 ≤ abs a

source

theorem abs_abs {α : Type u} [decidable_linear_ordered_add_comm_group α] (a : α) :

abs (abs a) = abs a

source

theorem le_abs_self {α : Type u} [decidable_linear_ordered_add_comm_group α] (a : α) :

a ≤ abs a

source

theorem neg_le_abs_self {α : Type u} [decidable_linear_ordered_add_comm_group α] (a : α) :

-a ≤ abs a

source

theorem eq_zero_of_abs_eq_zero {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} :

abs a = 0 → a = 0

source

theorem eq_of_abs_sub_eq_zero {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} :

abs (a - b) = 0 → a = b

source

theorem abs_pos_of_ne_zero {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} :

a ≠ 0 → 0 < abs a

source

theorem abs_by_cases {α : Type u} [decidable_linear_ordered_add_comm_group α] (P : α → Prop) {a : α} :

P a → P (-a) → P (abs a)

source

theorem abs_le_of_le_of_neg_le {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} :

a ≤ b → -a ≤ b → abs a ≤ b

source

theorem abs_lt_of_lt_of_neg_lt {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} :

a < b → -a < b → abs a < b

source

theorem abs_add_le_abs_add_abs {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :

abs (a + b) ≤ abs a + abs b

source

theorem abs_sub_abs_le_abs_sub {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :

abs a - abs b ≤ abs (a - b)

source

theorem abs_sub_le {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :

abs (a - c) ≤ abs (a - b) + abs (b - c)

source

theorem abs_add_three {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :

abs (a + b + c) ≤ abs a + abs b + abs c

source

theorem dist_bdd_within_interval {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b lb ub : α} :

lb ≤ a → a ≤ ub → lb ≤ b → b ≤ ub → abs (a - b) ≤ ub - lb

source

theorem decidable_linear_ordered_add_comm_group.eq_of_abs_sub_nonpos {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} :

abs (a - b) ≤ 0 → a = b

source

@[class]

structure nonneg_add_comm_group :

Type u_1 → Type u_1

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
neg : α → α
add_left_neg : ∀ (a : α), -a + a = 0
add_comm : ∀ (a b : α), a + b = b + a
nonneg : α → Prop
pos : α → Prop
pos_iff : (∀ (a : α), nonneg_add_comm_group.pos a ↔ nonneg_add_comm_group.nonneg a ∧ ¬nonneg_add_comm_group.nonneg (-a)) . "order_laws_tac"
zero_nonneg : nonneg_add_comm_group.nonneg 0
add_nonneg : ∀ {a b : α}, nonneg_add_comm_group.nonneg a → nonneg_add_comm_group.nonneg b → nonneg_add_comm_group.nonneg (a + b)
nonneg_antisymm : ∀ {a : α}, nonneg_add_comm_group.nonneg a → nonneg_add_comm_group.nonneg (-a) → a = 0