mathlib3 documentation

algebra.order.field.basic

Lemmas about linear ordered (semi)fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
def order_iso.mul_left₀ {α : Type u_2} [linear_ordered_semifield α] (a : α) (ha : 0 < a) :
α ≃o α

equiv.mul_left₀ as an order_iso.

Equations
source
@[simp]
theorem order_iso.mul_left₀_apply {α : Type u_2} [linear_ordered_semifield α] (a : α) (ha : 0 < a) (ᾰ : α) :
⇑(order_iso.mul_left₀ a ha) ᾰ = a * ᾰ
source
@[simp]
theorem order_iso.mul_left₀_symm_apply {α : Type u_2} [linear_ordered_semifield α] (a : α) (ha : 0 < a) (ᾰ : α) :
⇑(rel_iso.symm (order_iso.mul_left₀ a ha)) ᾰ = ↑(units.mk0 a _)⁻¹ * ᾰ
source
@[simp]
theorem order_iso.mul_right₀_symm_apply {α : Type u_2} [linear_ordered_semifield α] (a : α) (ha : 0 < a) (ᾰ : α) :
⇑(rel_iso.symm (order_iso.mul_right₀ a ha)) ᾰ = ᾰ * ↑(units.mk0 a _)⁻¹
source
def order_iso.mul_right₀ {α : Type u_2} [linear_ordered_semifield α] (a : α) (ha : 0 < a) :
α ≃o α

equiv.mul_right₀ as an order_iso.

Equations
source
@[simp]
theorem order_iso.mul_right₀_apply {α : Type u_2} [linear_ordered_semifield α] (a : α) (ha : 0 < a) (ᾰ : α) :
⇑(order_iso.mul_right₀ a ha) ᾰ = ᾰ * a

Lemmas about pos, nonneg, nonpos, neg #

source
@[simp]
theorem inv_pos {α : Type u_2} [linear_ordered_semifield α] {a : α} :
0 < a⁻¹ ↔ 0 < a
source
theorem inv_pos_of_pos {α : Type u_2} [linear_ordered_semifield α] {a : α} :
0 < a → 0 < a⁻¹

Alias of the reverse direction of inv_pos.

source
@[simp]
theorem inv_nonneg {α : Type u_2} [linear_ordered_semifield α] {a : α} :
0 ≤ a⁻¹ ↔ 0 ≤ a
source
theorem inv_nonneg_of_nonneg {α : Type u_2} [linear_ordered_semifield α] {a : α} :
0 ≤ a → 0 ≤ a⁻¹

Alias of the reverse direction of inv_nonneg.

source
@[simp]
theorem inv_lt_zero {α : Type u_2} [linear_ordered_semifield α] {a : α} :
a⁻¹ < 0 ↔ a < 0
source
@[simp]
theorem inv_nonpos {α : Type u_2} [linear_ordered_semifield α] {a : α} :
a⁻¹ ≤ 0 ↔ a ≤ 0
source
theorem one_div_pos {α : Type u_2} [linear_ordered_semifield α] {a : α} :
0 < 1 / a ↔ 0 < a
source
theorem one_div_neg {α : Type u_2} [linear_ordered_semifield α] {a : α} :
1 / a < 0 ↔ a < 0
source
theorem one_div_nonneg {α : Type u_2} [linear_ordered_semifield α] {a : α} :
0 ≤ 1 / a ↔ 0 ≤ a
source
theorem one_div_nonpos {α : Type u_2} [linear_ordered_semifield α] {a : α} :
1 / a ≤ 0 ↔ a ≤ 0
source
theorem div_pos {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a / b
source
theorem div_nonneg {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :
0 ≤ a / b
source
theorem div_nonpos_of_nonpos_of_nonneg {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : a ≤ 0) (hb : 0 ≤ b) :
a / b ≤ 0
source
theorem div_nonpos_of_nonneg_of_nonpos {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 ≤ a) (hb : b ≤ 0) :
a / b ≤ 0
source
theorem zpow_nonneg {α : Type u_2} [linear_ordered_semifield α] {a : α} (ha : 0 ≤ a) (n : ℤ) :
0 ≤ a ^ n
source
theorem zpow_pos_of_pos {α : Type u_2} [linear_ordered_semifield α] {a : α} (ha : 0 < a) (n : ℤ) :
0 < a ^ n

Relating one division with another term. #

source
theorem le_div_iff {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hc : 0 < c) :
a ≤ b / c ↔ a * c ≤ b
source
theorem le_div_iff' {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hc : 0 < c) :
a ≤ b / c ↔ c * a ≤ b
source
theorem div_le_iff {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hb : 0 < b) :
a / b ≤ c ↔ a ≤ c * b
source
theorem div_le_iff' {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hb : 0 < b) :
a / b ≤ c ↔ a ≤ b * c
source
theorem lt_div_iff {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hc : 0 < c) :
a < b / c ↔ a * c < b
source
theorem lt_div_iff' {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hc : 0 < c) :
a < b / c ↔ c * a < b
source
theorem div_lt_iff {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hc : 0 < c) :
b / c < a ↔ b < a * c
source
theorem div_lt_iff' {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hc : 0 < c) :
b / c < a ↔ b < c * a
source
theorem inv_mul_le_iff {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (h : 0 < b) :
b⁻¹ * a ≤ c ↔ a ≤ b * c
source
theorem inv_mul_le_iff' {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (h : 0 < b) :
b⁻¹ * a ≤ c ↔ a ≤ c * b
source
theorem mul_inv_le_iff {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (h : 0 < b) :
a * b⁻¹ ≤ c ↔ a ≤ b * c
source
theorem mul_inv_le_iff' {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (h : 0 < b) :
a * b⁻¹ ≤ c ↔ a ≤ c * b
source
theorem div_self_le_one {α : Type u_2} [linear_ordered_semifield α] (a : α) :
a / a ≤ 1
source
theorem inv_mul_lt_iff {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (h : 0 < b) :
b⁻¹ * a < c ↔ a < b * c
source
theorem inv_mul_lt_iff' {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (h : 0 < b) :
b⁻¹ * a < c ↔ a < c * b
source
theorem mul_inv_lt_iff {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (h : 0 < b) :
a * b⁻¹ < c ↔ a < b * c
source
theorem mul_inv_lt_iff' {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (h : 0 < b) :
a * b⁻¹ < c ↔ a < c * b
source
theorem inv_pos_le_iff_one_le_mul {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) :
a⁻¹ ≤ b ↔ 1 ≤ b * a
source
theorem inv_pos_le_iff_one_le_mul' {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) :
a⁻¹ ≤ b ↔ 1 ≤ a * b
source
theorem inv_pos_lt_iff_one_lt_mul {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) :
a⁻¹ < b ↔ 1 < b * a
source
theorem inv_pos_lt_iff_one_lt_mul' {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) :
a⁻¹ < b ↔ 1 < a * b
source
theorem div_le_of_nonneg_of_le_mul {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c * b) :
a / b ≤ c

One direction of div_le_iff where b is allowed to be 0 (but c must be nonnegative)

source
theorem mul_le_of_nonneg_of_le_div {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ b / c) :
a * c ≤ b

One direction of div_le_iff where c is allowed to be 0 (but b must be nonnegative)

source
theorem div_le_one_of_le {α : Type u_2} [linear_ordered_semifield α] {a b : α} (h : a ≤ b) (hb : 0 ≤ b) :
a / b ≤ 1

Bi-implications of inequalities using inversions #

source
theorem inv_le_inv_of_le {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (h : a ≤ b) :
b⁻¹ ≤ a⁻¹
source
theorem inv_le_inv {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
a⁻¹ ≤ b⁻¹ ↔ b ≤ a

See inv_le_inv_of_le for the implication from right-to-left with one fewer assumption.

source
theorem inv_le {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
a⁻¹ ≤ b ↔ b⁻¹ ≤ a

In a linear ordered field, for positive a and b we have a⁻¹ ≤ b ↔ b⁻¹ ≤ a. See also inv_le_of_inv_le for a one-sided implication with one fewer assumption.

source
theorem inv_le_of_inv_le {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (h : a⁻¹ ≤ b) :
b⁻¹ ≤ a
source
theorem le_inv {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
a ≤ b⁻¹ ↔ b ≤ a⁻¹
source
theorem inv_lt_inv {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
a⁻¹ < b⁻¹ ↔ b < a

See inv_lt_inv_of_lt for the implication from right-to-left with one fewer assumption.

source
theorem inv_lt_inv_of_lt {α : Type u_2} [linear_ordered_semifield α] {a b : α} (hb : 0 < b) (h : b < a) :
a⁻¹ < b⁻¹
source
theorem inv_lt {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
a⁻¹ < b ↔ b⁻¹ < a

In a linear ordered field, for positive a and b we have a⁻¹ < b ↔ b⁻¹ < a. See also inv_lt_of_inv_lt for a one-sided implication with one fewer assumption.

source
theorem inv_lt_of_inv_lt {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (h : a⁻¹ < b) :
b⁻¹ < a
source
theorem lt_inv {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
a < b⁻¹ ↔ b < a⁻¹
source
theorem inv_lt_one {α : Type u_2} [linear_ordered_semifield α] {a : α} (ha : 1 < a) :
a⁻¹ < 1
source
theorem one_lt_inv {α : Type u_2} [linear_ordered_semifield α] {a : α} (h₁ : 0 < a) (h₂ : a < 1) :
1 < a⁻¹
source
theorem inv_le_one {α : Type u_2} [linear_ordered_semifield α] {a : α} (ha : 1 ≤ a) :
a⁻¹ ≤ 1
source
theorem one_le_inv {α : Type u_2} [linear_ordered_semifield α] {a : α} (h₁ : 0 < a) (h₂ : a ≤ 1) :
1 ≤ a⁻¹
source
theorem inv_lt_one_iff_of_pos {α : Type u_2} [linear_ordered_semifield α] {a : α} (h₀ : 0 < a) :
a⁻¹ < 1 ↔ 1 < a
source
theorem inv_lt_one_iff {α : Type u_2} [linear_ordered_semifield α] {a : α} :
a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a
source
theorem one_lt_inv_iff {α : Type u_2} [linear_ordered_semifield α] {a : α} :
1 < a⁻¹ ↔ 0 < a ∧ a < 1
source
theorem inv_le_one_iff {α : Type u_2} [linear_ordered_semifield α] {a : α} :
a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a
source
theorem one_le_inv_iff {α : Type u_2} [linear_ordered_semifield α] {a : α} :
1 ≤ a⁻¹ ↔ 0 < a ∧ a ≤ 1

Relating two divisions. #

source
theorem div_le_div_of_le {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hc : 0 ≤ c) (h : a ≤ b) :
a / c ≤ b / c
source
theorem div_le_div_of_le_left {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (ha : 0 ≤ a) (hc : 0 < c) (h : c ≤ b) :
a / b ≤ a / c
source
theorem div_le_div_of_le_of_nonneg {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hab : a ≤ b) (hc : 0 ≤ c) :
a / c ≤ b / c
source
theorem div_lt_div_of_lt {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hc : 0 < c) (h : a < b) :
a / c < b / c
source
theorem div_le_div_right {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hc : 0 < c) :
a / c ≤ b / c ↔ a ≤ b
source
theorem div_lt_div_right {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hc : 0 < c) :
a / c < b / c ↔ a < b
source
theorem div_lt_div_left {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a / b < a / c ↔ c < b
source
theorem div_le_div_left {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a / b ≤ a / c ↔ c ≤ b
source
theorem div_lt_div_iff {α : Type u_2} [linear_ordered_semifield α] {a b c d : α} (b0 : 0 < b) (d0 : 0 < d) :
a / b < c / d ↔ a * d < c * b
source
theorem div_le_div_iff {α : Type u_2} [linear_ordered_semifield α] {a b c d : α} (b0 : 0 < b) (d0 : 0 < d) :
a / b ≤ c / d ↔ a * d ≤ c * b
source
theorem div_le_div {α : Type u_2} [linear_ordered_semifield α] {a b c d : α} (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hbd : d ≤ b) :
a / b ≤ c / d
source
theorem div_lt_div {α : Type u_2} [linear_ordered_semifield α] {a b c d : α} (hac : a < c) (hbd : d ≤ b) (c0 : 0 ≤ c) (d0 : 0 < d) :
a / b < c / d
source
theorem div_lt_div' {α : Type u_2} [linear_ordered_semifield α] {a b c d : α} (hac : a ≤ c) (hbd : d < b) (c0 : 0 < c) (d0 : 0 < d) :
a / b < c / d
source
theorem div_lt_div_of_lt_left {α : Type u_2} [linear_ordered_semifield α] {a b c : α} (hc : 0 < c) (hb : 0 < b) (h : b < a) :
c / a < c / b

Relating one division and involving 1 #

source
theorem div_le_self {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 ≤ a) (hb : 1 ≤ b) :
a / b ≤ a
source
theorem div_lt_self {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 1 < b) :
a / b < a
source
theorem le_div_self {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 ≤ a) (hb₀ : 0 < b) (hb₁ : b ≤ 1) :
a ≤ a / b
source
theorem one_le_div {α : Type u_2} [linear_ordered_semifield α] {a b : α} (hb : 0 < b) :
1 ≤ a / b ↔ b ≤ a
source
theorem div_le_one {α : Type u_2} [linear_ordered_semifield α] {a b : α} (hb : 0 < b) :
a / b ≤ 1 ↔ a ≤ b
source
theorem one_lt_div {α : Type u_2} [linear_ordered_semifield α] {a b : α} (hb : 0 < b) :
1 < a / b ↔ b < a
source
theorem div_lt_one {α : Type u_2} [linear_ordered_semifield α] {a b : α} (hb : 0 < b) :
a / b < 1 ↔ a < b
source
theorem one_div_le {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
1 / a ≤ b ↔ 1 / b ≤ a
source
theorem one_div_lt {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
1 / a < b ↔ 1 / b < a
source
theorem le_one_div {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
a ≤ 1 / b ↔ b ≤ 1 / a
source
theorem lt_one_div {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
a < 1 / b ↔ b < 1 / a

Relating two divisions, involving 1 #

source
theorem one_div_le_one_div_of_le {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (h : a ≤ b) :
1 / b ≤ 1 / a
source
theorem one_div_lt_one_div_of_lt {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (h : a < b) :
1 / b < 1 / a
source
theorem le_of_one_div_le_one_div {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (h : 1 / a ≤ 1 / b) :
b ≤ a
source
theorem lt_of_one_div_lt_one_div {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (h : 1 / a < 1 / b) :
b < a
source
theorem one_div_le_one_div {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
1 / a ≤ 1 / b ↔ b ≤ a

For the single implications with fewer assumptions, see one_div_le_one_div_of_le and le_of_one_div_le_one_div

source
theorem one_div_lt_one_div {α : Type u_2} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
1 / a < 1 / b ↔ b < a

For the single implications with fewer assumptions, see one_div_lt_one_div_of_lt and lt_of_one_div_lt_one_div

source
theorem one_lt_one_div {α : Type u_2} [linear_ordered_semifield α] {a : α} (h1 : 0 < a) (h2 : a < 1) :
1 < 1 / a
source
theorem one_le_one_div {α : Type u_2} [linear_ordered_semifield α] {a : α} (h1 : 0 < a) (h2 : a ≤ 1) :
1 ≤ 1 / a

Results about halving. #

The equalities also hold in semifields of characteristic 0.

source
theorem add_halves {α : Type u_2} [linear_ordered_semifield α] (a : α) :
a / 2 + a / 2 = a
source
theorem add_self_div_two {α : Type u_2} [linear_ordered_semifield α] (a : α) :
(a + a) / 2 = a
source
theorem half_pos {α : Type u_2} [linear_ordered_semifield α] {a : α} (h : 0 < a) :
0 < a / 2
source
theorem one_half_pos {α : Type u_2} [linear_ordered_semifield α] :
0 < 1 / 2
source
@[simp]
theorem half_le_self_iff {α : Type u_2} [linear_ordered_semifield α] {a : α} :
a / 2 ≤ a ↔ 0 ≤ a
source
@[simp]
theorem half_lt_self_iff {α : Type u_2} [linear_ordered_semifield α] {a : α} :
a / 2 < a ↔ 0 < a
source
theorem half_le_self {α : Type u_2} [linear_ordered_semifield α] {a : α} :
0 ≤ a → a / 2 ≤ a

Alias of the reverse direction of half_le_self_iff.

source
theorem half_lt_self {α : Type u_2} [linear_ordered_semifield α] {a : α} :
0 < a → a / 2 < a

Alias of the reverse direction of half_lt_self_iff.

source
theorem div_two_lt_of_pos {α : Type u_2} [linear_ordered_semifield α] {a : α} :
0 < a → a / 2 < a

Alias of half_lt_self.

source
theorem one_half_lt_one {α : Type u_2} [linear_ordered_semifield α] :
1 / 2 < 1
source
theorem two_inv_lt_one {α : Type u_2} [linear_ordered_semifield α] :
2⁻¹ < 1
source
theorem left_lt_add_div_two {α : Type u_2} [linear_ordered_semifield α] {a b : α} :
a < (a + b) / 2 ↔ a < b
source
theorem add_div_two_lt_right {α : Type u_2} [linear_ordered_semifield α] {a b : α} :
(a + b) / 2 < b ↔ a < b

Miscellaneous lemmas #

source
theorem mul_le_mul_of_mul_div_le {α : Type u_2} [linear_ordered_semifield α] {a b c d : α} (h : a * (b / c) ≤ d) (hc : 0 < c) :
b * a ≤ d * c
source
theorem div_mul_le_div_mul_of_div_le_div {α : Type u_2} [linear_ordered_semifield α] {a b c d e : α} (h : a / b ≤ c / d) (he : 0 ≤ e) :
a / (b * e) ≤ c / (d * e)
source
theorem exists_pos_mul_lt {α : Type u_2} [linear_ordered_semifield α] {a : α} (h : 0 < a) (b : α) :
∃ (c : α), 0 < c ∧ b * c < a
source
theorem exists_pos_lt_mul {α : Type u_2} [linear_ordered_semifield α] {a : α} (h : 0 < a) (b : α) :
∃ (c : α), 0 < c ∧ b < c * a
source
theorem monotone.div_const {α : Type u_2} [linear_ordered_semifield α] {β : Type u_1} [preorder β] {f : β → α} (hf : monotone f) {c : α} (hc : 0 ≤ c) :
monotone (λ (x : β), f x / c)
source
theorem strict_mono.div_const {α : Type u_2} [linear_ordered_semifield α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) {c : α} (hc : 0 < c) :
strict_mono (λ (x : β), f x / c)
source
@[protected, instance]
def linear_ordered_semifield.to_densely_ordered {α : Type u_2} [linear_ordered_semifield α] :
densely_ordered α
source
theorem min_div_div_right {α : Type u_2} [linear_ordered_semifield α] {c : α} (hc : 0 ≤ c) (a b : α) :
linear_order.min (a / c) (b / c) = linear_order.min a b / c
source
theorem max_div_div_right {α : Type u_2} [linear_ordered_semifield α] {c : α} (hc : 0 ≤ c) (a b : α) :
linear_order.max (a / c) (b / c) = linear_order.max a b / c
source
theorem one_div_strict_anti_on {α : Type u_2} [linear_ordered_semifield α] :
strict_anti_on (λ (x : α), 1 / x) (set.Ioi 0)
source
theorem one_div_pow_le_one_div_pow_of_le {α : Type u_2} [linear_ordered_semifield α] {a : α} (a1 : 1 ≤ a) {m n : ℕ} (mn : m ≤ n) :
1 / a ^ n ≤ 1 / a ^ m
source
theorem one_div_pow_lt_one_div_pow_of_lt {α : Type u_2} [linear_ordered_semifield α] {a : α} (a1 : 1 < a) {m n : ℕ} (mn : m < n) :
1 / a ^ n < 1 / a ^ m
source
theorem one_div_pow_anti {α : Type u_2} [linear_ordered_semifield α] {a : α} (a1 : 1 ≤ a) :
antitone (λ (n : ℕ), 1 / a ^ n)
source
theorem one_div_pow_strict_anti {α : Type u_2} [linear_ordered_semifield α] {a : α} (a1 : 1 < a) :
strict_anti (λ (n : ℕ), 1 / a ^ n)
source
theorem inv_strict_anti_on {α : Type u_2} [linear_ordered_semifield α] :
strict_anti_on (λ (x : α), x⁻¹) (set.Ioi 0)
source
theorem inv_pow_le_inv_pow_of_le {α : Type u_2} [linear_ordered_semifield α] {a : α} (a1 : 1 ≤ a) {m n : ℕ} (mn : m ≤ n) :
(a ^ n)⁻¹ ≤ (a ^ m)⁻¹
source
theorem inv_pow_lt_inv_pow_of_lt {α : Type u_2} [linear_ordered_semifield α] {a : α} (a1 : 1 < a) {m n : ℕ} (mn : m < n) :
(a ^ n)⁻¹ < (a ^ m)⁻¹
source
theorem inv_pow_anti {α : Type u_2} [linear_ordered_semifield α] {a : α} (a1 : 1 ≤ a) :
antitone (λ (n : ℕ), (a ^ n)⁻¹)
source
theorem inv_pow_strict_anti {α : Type u_2} [linear_ordered_semifield α] {a : α} (a1 : 1 < a) :
strict_anti (λ (n : ℕ), (a ^ n)⁻¹)

Results about is_lub and is_glb #

source
theorem is_glb.mul_left {α : Type u_2} [linear_ordered_semifield α] {a b : α} {s : set α} (ha : 0 ≤ a) (hs : is_glb s b) :
is_glb ((λ (b : α), a * b) '' s) (a * b)
source
theorem is_glb.mul_right {α : Type u_2} [linear_ordered_semifield α] {a b : α} {s : set α} (ha : 0 ≤ a) (hs : is_glb s b) :
is_glb ((λ (b : α), b * a) '' s) (b * a)

Lemmas about pos, nonneg, nonpos, neg #

source
theorem div_pos_iff {α : Type u_2} [linear_ordered_field α] {a b : α} :
0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
source
theorem div_neg_iff {α : Type u_2} [linear_ordered_field α] {a b : α} :
a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
source
theorem div_nonneg_iff {α : Type u_2} [linear_ordered_field α] {a b : α} :
0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
source
theorem div_nonpos_iff {α : Type u_2} [linear_ordered_field α] {a b : α} :
a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
source
theorem div_nonneg_of_nonpos {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) :
0 ≤ a / b
source
theorem div_pos_of_neg_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
0 < a / b
source
theorem div_neg_of_neg_of_pos {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : 0 < b) :
a / b < 0
source
theorem div_neg_of_pos_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : 0 < a) (hb : b < 0) :
a / b < 0

Relating one division with another term #

source
theorem div_le_iff_of_neg {α : Type u_2} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
b / c ≤ a ↔ a * c ≤ b
source
theorem div_le_iff_of_neg' {α : Type u_2} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
b / c ≤ a ↔ c * a ≤ b
source
theorem le_div_iff_of_neg {α : Type u_2} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
a ≤ b / c ↔ b ≤ a * c
source
theorem le_div_iff_of_neg' {α : Type u_2} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
a ≤ b / c ↔ b ≤ c * a
source
theorem div_lt_iff_of_neg {α : Type u_2} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
b / c < a ↔ a * c < b
source
theorem div_lt_iff_of_neg' {α : Type u_2} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
b / c < a ↔ c * a < b
source
theorem lt_div_iff_of_neg {α : Type u_2} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
a < b / c ↔ b < a * c
source
theorem lt_div_iff_of_neg' {α : Type u_2} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
a < b / c ↔ b < c * a
source
theorem div_le_one_of_ge {α : Type u_2} [linear_ordered_field α] {a b : α} (h : b ≤ a) (hb : b ≤ 0) :
a / b ≤ 1

Bi-implications of inequalities using inversions #

source
theorem inv_le_inv_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
a⁻¹ ≤ b⁻¹ ↔ b ≤ a
source
theorem inv_le_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
a⁻¹ ≤ b ↔ b⁻¹ ≤ a
source
theorem le_inv_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
a ≤ b⁻¹ ↔ b ≤ a⁻¹
source
theorem inv_lt_inv_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
a⁻¹ < b⁻¹ ↔ b < a
source
theorem inv_lt_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
a⁻¹ < b ↔ b⁻¹ < a
source
theorem lt_inv_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
a < b⁻¹ ↔ b < a⁻¹

Relating two divisions #

source
theorem div_le_div_of_nonpos_of_le {α : Type u_2} [linear_ordered_field α] {a b c : α} (hc : c ≤ 0) (h : b ≤ a) :
a / c ≤ b / c
source
theorem div_lt_div_of_neg_of_lt {α : Type u_2} [linear_ordered_field α] {a b c : α} (hc : c < 0) (h : b < a) :
a / c < b / c
source
theorem div_le_div_right_of_neg {α : Type u_2} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
a / c ≤ b / c ↔ b ≤ a
source
theorem div_lt_div_right_of_neg {α : Type u_2} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
a / c < b / c ↔ b < a

Relating one division and involving 1 #

source
theorem one_le_div_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (hb : b < 0) :
1 ≤ a / b ↔ a ≤ b
source
theorem div_le_one_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (hb : b < 0) :
a / b ≤ 1 ↔ b ≤ a
source
theorem one_lt_div_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (hb : b < 0) :
1 < a / b ↔ a < b
source
theorem div_lt_one_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (hb : b < 0) :
a / b < 1 ↔ b < a
source
theorem one_div_le_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
1 / a ≤ b ↔ 1 / b ≤ a
source
theorem one_div_lt_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
1 / a < b ↔ 1 / b < a
source
theorem le_one_div_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
a ≤ 1 / b ↔ b ≤ 1 / a
source
theorem lt_one_div_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
a < 1 / b ↔ b < 1 / a
source
theorem one_lt_div_iff {α : Type u_2} [linear_ordered_field α] {a b : α} :
1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
source
theorem one_le_div_iff {α : Type u_2} [linear_ordered_field α] {a b : α} :
1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
source
theorem div_lt_one_iff {α : Type u_2} [linear_ordered_field α] {a b : α} :
a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
source
theorem div_le_one_iff {α : Type u_2} [linear_ordered_field α] {a b : α} :
a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

Relating two divisions, involving 1 #

source
theorem one_div_le_one_div_of_neg_of_le {α : Type u_2} [linear_ordered_field α] {a b : α} (hb : b < 0) (h : a ≤ b) :
1 / b ≤ 1 / a
source
theorem one_div_lt_one_div_of_neg_of_lt {α : Type u_2} [linear_ordered_field α] {a b : α} (hb : b < 0) (h : a < b) :
1 / b < 1 / a
source
theorem le_of_neg_of_one_div_le_one_div {α : Type u_2} [linear_ordered_field α] {a b : α} (hb : b < 0) (h : 1 / a ≤ 1 / b) :
b ≤ a
source
theorem lt_of_neg_of_one_div_lt_one_div {α : Type u_2} [linear_ordered_field α] {a b : α} (hb : b < 0) (h : 1 / a < 1 / b) :
b < a
source
theorem one_div_le_one_div_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
1 / a ≤ 1 / b ↔ b ≤ a

For the single implications with fewer assumptions, see one_div_lt_one_div_of_neg_of_lt and lt_of_one_div_lt_one_div

source
theorem one_div_lt_one_div_of_neg {α : Type u_2} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
1 / a < 1 / b ↔ b < a

For the single implications with fewer assumptions, see one_div_lt_one_div_of_lt and lt_of_one_div_lt_one_div

source
theorem one_div_lt_neg_one {α : Type u_2} [linear_ordered_field α] {a : α} (h1 : a < 0) (h2 : -1 < a) :
1 / a < -1
source
theorem one_div_le_neg_one {α : Type u_2} [linear_ordered_field α] {a : α} (h1 : a < 0) (h2 : -1 ≤ a) :
1 / a ≤ -1

Results about halving #

source
theorem sub_self_div_two {α : Type u_2} [linear_ordered_field α] (a : α) :
a - a / 2 = a / 2
source
theorem div_two_sub_self {α : Type u_2} [linear_ordered_field α] (a : α) :
a / 2 - a = -(a / 2)
source
theorem add_sub_div_two_lt {α : Type u_2} [linear_ordered_field α] {a b : α} (h : a < b) :
a + (b - a) / 2 < b
source
theorem sub_one_div_inv_le_two {α : Type u_2} [linear_ordered_field α] {a : α} (a2 : 2 ≤ a) :
(1 - 1 / a)⁻¹ ≤ 2

An inequality involving 2.

Results about is_lub and is_glb #

source
theorem is_lub.mul_left {α : Type u_2} [linear_ordered_field α] {a b : α} {s : set α} (ha : 0 ≤ a) (hs : is_lub s b) :
is_lub ((λ (b : α), a * b) '' s) (a * b)
source
theorem is_lub.mul_right {α : Type u_2} [linear_ordered_field α] {a b : α} {s : set α} (ha : 0 ≤ a) (hs : is_lub s b) :
is_lub ((λ (b : α), b * a) '' s) (b * a)

Miscellaneous lemmmas #

source
theorem mul_sub_mul_div_mul_neg_iff {α : Type u_2} [linear_ordered_field α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) :
(a * d - b * c) / (c * d) < 0 ↔ a / c < b / d
source
theorem mul_sub_mul_div_mul_nonpos_iff {α : Type u_2} [linear_ordered_field α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) :
(a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d
source
theorem mul_sub_mul_div_mul_neg {α : Type u_2} [linear_ordered_field α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) :
a / c < b / d → (a * d - b * c) / (c * d) < 0

Alias of the reverse direction of mul_sub_mul_div_mul_neg_iff.

source
theorem div_lt_div_of_mul_sub_mul_div_neg {α : Type u_2} [linear_ordered_field α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) :
(a * d - b * c) / (c * d) < 0 → a / c < b / d

Alias of the forward direction of mul_sub_mul_div_mul_neg_iff.

source
theorem mul_sub_mul_div_mul_nonpos {α : Type u_2} [linear_ordered_field α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) :
a / c ≤ b / d → (a * d - b * c) / (c * d) ≤ 0

Alias of the reverse direction of mul_sub_mul_div_mul_nonpos_iff.

source
theorem div_le_div_of_mul_sub_mul_div_nonpos {α : Type u_2} [linear_ordered_field α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) :
(a * d - b * c) / (c * d) ≤ 0 → a / c ≤ b / d

Alias of the forward direction of mul_sub_mul_div_mul_nonpos_iff.

source
theorem exists_add_lt_and_pos_of_lt {α : Type u_2} [linear_ordered_field α] {a b : α} (h : b < a) :
∃ (c : α), b + c < a ∧ 0 < c
source
theorem le_of_forall_sub_le {α : Type u_2} [linear_ordered_field α] {a b : α} (h : ∀ (ε : α), ε > 0 → b - ε ≤ a) :
b ≤ a
source
theorem mul_self_inj_of_nonneg {α : Type u_2} [linear_ordered_field α] {a b : α} (a0 : 0 ≤ a) (b0 : 0 ≤ b) :
a * a = b * b ↔ a = b
source
theorem min_div_div_right_of_nonpos {α : Type u_2} [linear_ordered_field α] {c : α} (hc : c ≤ 0) (a b : α) :
linear_order.min (a / c) (b / c) = linear_order.max a b / c
source
theorem max_div_div_right_of_nonpos {α : Type u_2} [linear_ordered_field α] {c : α} (hc : c ≤ 0) (a b : α) :
linear_order.max (a / c) (b / c) = linear_order.min a b / c
source
theorem abs_inv {α : Type u_2} [linear_ordered_field α] (a : α) :
|a⁻¹| = |a|⁻¹
source
theorem abs_div {α : Type u_2} [linear_ordered_field α] (a b : α) :
|a / b| = |a| / |b|
source
theorem abs_one_div {α : Type u_2} [linear_ordered_field α] (a : α) :
|1 / a| = 1 / |a|