doc-next-gen

Mathlib.Algebra.Order.Field.Basic

Module docstring

{"# Lemmas about linear ordered (semi)fields ","### Relating two divisions. ","### Relating one division and involving 1 ","### Relating two divisions, involving 1 ","### Results about halving. The equalities also hold in semifields of characteristic 0. ","### Miscellaneous lemmas ","### Results about IsGLB ","### Lemmas about pos, nonneg, nonpos, neg ","### Relating one division with another term ","### Bi-implications of inequalities using inversions ","### Monotonicity results involving inversion ","### Relating two divisions ","### Relating one division and involving 1 ","### Relating two divisions, involving 1 ","### Results about halving ","### Results about IsLUB ","### Miscellaneous lemmas "}

div_le_div_right theorem
(hc : 0 < c) : a / c ≤ b / c ↔ a ≤ b
Full source 
@[deprecated div_le_div_iff_of_pos_right (since := "2024-11-12")]
theorem div_le_div_right (hc : 0 < c) : a / c ≤ b / c ↔ a ≤ b := div_le_div_iff_of_pos_right hc
Division Preserves Order for Positive Denominator: $\frac{a}{c} \leq \frac{b}{c} \leftrightarrow a \leq b$
Informal description
For any positive element $c$ in a linearly ordered field, the inequality $\frac{a}{c} \leq \frac{b}{c}$ holds if and only if $a \leq b$.
div_lt_div_right theorem
(hc : 0 < c) : a / c < b / c ↔ a < b
Full source 
@[deprecated div_lt_div_iff_of_pos_right (since := "2024-11-12")]
theorem div_lt_div_right (hc : 0 < c) : a / c < b / c ↔ a < b := div_lt_div_iff_of_pos_right hc
Division Preserves Strict Order for Positive Elements: $a / c < b / c \leftrightarrow a < b$ when $c > 0$
Informal description
For any positive element $c$ in a linearly ordered field, the inequality $a / c < b / c$ holds if and only if $a < b$.
div_lt_div_left theorem
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b < a / c ↔ c < b
Full source 
@[deprecated div_lt_div_iff_of_pos_left (since := "2024-11-13")]
theorem div_lt_div_left (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b < a / c ↔ c < b :=
  div_lt_div_iff_of_pos_left ha hb hc
Strict Division Inequality for Positive Elements: $\frac{a}{b} < \frac{a}{c} \leftrightarrow c < b$ when $a, b, c > 0$
Informal description
For any positive real numbers $a, b, c > 0$, the strict inequality $\frac{a}{b} < \frac{a}{c}$ holds if and only if $c < b$.
div_le_div_left theorem
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b ≤ a / c ↔ c ≤ b
Full source 
@[deprecated div_le_div_iff_of_pos_left (since := "2024-11-12")]
theorem div_le_div_left (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b ≤ a / c ↔ c ≤ b :=
  div_le_div_iff_of_pos_left ha hb hc
Division Inequality for Positive Elements: $\frac{a}{b} \leq \frac{a}{c} \leftrightarrow c \leq b$ when $a, b, c > 0$
Informal description
For any positive real numbers $a, b, c > 0$, the inequality $\frac{a}{b} \leq \frac{a}{c}$ holds if and only if $c \leq b$.
div_lt_div_iff theorem
(b0 : 0 < b) (d0 : 0 < d) : a / b < c / d ↔ a * d < c * b
Full source 
@[deprecated div_lt_div_iff₀ (since := "2024-11-12")]
theorem div_lt_div_iff (b0 : 0 < b) (d0 : 0 < d) : a / b < c / d ↔ a * d < c * b :=
  div_lt_div_iff₀ b0 d0
Fraction Inequality Criterion: $\frac{a}{b} < \frac{c}{d} \leftrightarrow a \cdot d < c \cdot b$ for $b, d > 0$
Informal description
For any positive real numbers $b$ and $d$, the inequality $\frac{a}{b} < \frac{c}{d}$ holds if and only if $a \cdot d < c \cdot b$.
div_le_div_iff theorem
(b0 : 0 < b) (d0 : 0 < d) : a / b ≤ c / d ↔ a * d ≤ c * b
Full source 
@[deprecated div_le_div_iff₀ (since := "2024-11-12")]
theorem div_le_div_iff (b0 : 0 < b) (d0 : 0 < d) : a / b ≤ c / d ↔ a * d ≤ c * b :=
  div_le_div_iff₀ b0 d0
Division Inequality Equivalence: $\frac{a}{b} \leq \frac{c}{d} \leftrightarrow a \cdot d \leq c \cdot b$ for $b, d > 0$
Informal description
For any positive real numbers $b$ and $d$, the inequality $\frac{a}{b} \leq \frac{c}{d}$ holds if and only if $a \cdot d \leq c \cdot b$.
div_le_div theorem
(hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hbd : d ≤ b) : a / b ≤ c / d
Full source 
@[deprecated div_le_div₀ (since := "2024-11-12")]
theorem div_le_div (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hbd : d ≤ b) : a / b ≤ c / d :=
  div_le_div₀ hc hac hd hbd
Division Inequality: $\frac{a}{b} \leq \frac{c}{d}$ under Nonnegative Conditions
Informal description
For any elements $a, b, c, d$ in a linearly ordered field, if $0 \leq c$, $a \leq c$, $0 < d$, and $d \leq b$, then the inequality $\frac{a}{b} \leq \frac{c}{d}$ holds.
div_lt_div theorem
(hac : a < c) (hbd : d ≤ b) (c0 : 0 ≤ c) (d0 : 0 < d) : a / b < c / d
Full source 
@[deprecated div_lt_div₀ (since := "2024-11-12")]
theorem div_lt_div (hac : a < c) (hbd : d ≤ b) (c0 : 0 ≤ c) (d0 : 0 < d) : a / b < c / d :=
  div_lt_div₀ hac hbd c0 d0
Fraction Inequality: $\frac{a}{b} < \frac{c}{d}$ under Partial Order Conditions
Informal description
For any elements $a, b, c, d$ in a linearly ordered field, if $a < c$, $d \leq b$, $0 \leq c$, and $0 < d$, then the inequality $\frac{a}{b} < \frac{c}{d}$ holds.
div_lt_div' theorem
(hac : a ≤ c) (hbd : d < b) (c0 : 0 < c) (d0 : 0 < d) : a / b < c / d
Full source 
@[deprecated div_lt_div₀' (since := "2024-11-12")]
theorem div_lt_div' (hac : a ≤ c) (hbd : d < b) (c0 : 0 < c) (d0 : 0 < d) : a / b < c / d :=
  div_lt_div₀' hac hbd c0 d0
Fraction Inequality under Partial Order: $\frac{a}{b} < \frac{c}{d}$ when $a \leq c$, $d < b$, and $c, d > 0$
Informal description
For elements $a, b, c, d$ in a linearly ordered field with $0 < c$, $0 < d$, $a \leq c$, and $d < b$, the inequality $\frac{a}{b} < \frac{c}{d}$ holds.
div_le_self theorem
(ha : 0 ≤ a) (hb : 1 ≤ b) : a / b ≤ a
Full source 
@[bound]
theorem div_le_self (ha : 0 ≤ a) (hb : 1 ≤ b) : a / b ≤ a := by
  simpa only [div_one] using div_le_div_of_nonneg_left ha zero_lt_one hb
Nonnegative Division Inequality: $a/b \leq a$ for $a \geq 0$, $b \geq 1$
Informal description
For any nonnegative element $a$ and any element $b \geq 1$ in a linearly ordered field, the inequality $a / b \leq a$ holds.
div_lt_self theorem
(ha : 0 < a) (hb : 1 < b) : a / b < a
Full source 
@[bound]
theorem div_lt_self (ha : 0 < a) (hb : 1 < b) : a / b < a := by
  simpa only [div_one] using div_lt_div_of_pos_left ha zero_lt_one hb
Strict Inequality for Division by Greater Than One: $\frac{a}{b} < a$ when $a > 0$ and $b > 1$
Informal description
For any positive real number $a$ and any real number $b$ such that $a > 0$ and $b > 1$, the inequality $\frac{a}{b} < a$ holds.
le_div_self theorem
(ha : 0 ≤ a) (hb₀ : 0 < b) (hb₁ : b ≤ 1) : a ≤ a / b
Full source 
@[bound]
theorem le_div_self (ha : 0 ≤ a) (hb₀ : 0 < b) (hb₁ : b ≤ 1) : a ≤ a / b := by
  simpa only [div_one] using div_le_div_of_nonneg_left ha hb₀ hb₁
Nonnegative Element Inequality: $a \leq a/b$ for $a \geq 0$, $0 < b \leq 1$
Informal description
For any nonnegative element $a$ and positive element $b \leq 1$ in a linear ordered field, it holds that $a \leq a / b$.
one_le_div theorem
(hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a
Full source 
theorem one_le_div (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a := by rw [le_div_iff₀ hb, one_mul]
Inequality Equivalence: $1 \leq a/b \leftrightarrow b \leq a$ for $b > 0$
Informal description
For any elements $a$ and $b$ in a linear ordered field with $b > 0$, the inequality $1 \leq a / b$ holds if and only if $b \leq a$.
div_le_one theorem
(hb : 0 < b) : a / b ≤ 1 ↔ a ≤ b
Full source 
theorem div_le_one (hb : 0 < b) : a / b ≤ 1 ↔ a ≤ b := by rw [div_le_iff₀ hb, one_mul]
Division Inequality: $\frac{a}{b} \leq 1 \leftrightarrow a \leq b$ for $b > 0$
Informal description
For any positive element $b$ in a linear ordered field, the inequality $\frac{a}{b} \leq 1$ holds if and only if $a \leq b$.
one_lt_div theorem
(hb : 0 < b) : 1 < a / b ↔ b < a
Full source 
theorem one_lt_div (hb : 0 < b) : 1 < a / b ↔ b < a := by rw [lt_div_iff₀ hb, one_mul]
Inequality equivalence: $1 < a/b \leftrightarrow b < a$ for $b > 0$
Informal description
For any elements $a$ and $b$ in a linear ordered field, if $b > 0$, then $1 < a / b$ if and only if $b < a$.
div_lt_one theorem
(hb : 0 < b) : a / b < 1 ↔ a < b
Full source 
theorem div_lt_one (hb : 0 < b) : a / b < 1 ↔ a < b := by rw [div_lt_iff₀ hb, one_mul]
Division by Positive Number Less Than One: $\frac{a}{b} < 1 \leftrightarrow a < b$
Informal description
For any positive real number $b > 0$, the inequality $\frac{a}{b} < 1$ holds if and only if $a < b$.
one_div_le theorem
(ha : 0 < a) (hb : 0 < b) : 1 / a ≤ b ↔ 1 / b ≤ a
Full source 
theorem one_div_le (ha : 0 < a) (hb : 0 < b) : 1 / a ≤ b ↔ 1 / b ≤ a := by
  simpa using inv_le_comm₀ ha hb
Reciprocal Inequality Equivalence: $\frac{1}{a} \leq b \leftrightarrow \frac{1}{b} \leq a$ for $a, b > 0$
Informal description
For any positive elements $a$ and $b$ in a linear ordered field, the inequality $\frac{1}{a} \leq b$ holds if and only if $\frac{1}{b} \leq a$.
one_div_lt theorem
(ha : 0 < a) (hb : 0 < b) : 1 / a < b ↔ 1 / b < a
Full source 
theorem one_div_lt (ha : 0 < a) (hb : 0 < b) : 1 / a < b ↔ 1 / b < a := by
  simpa using inv_lt_comm₀ ha hb
Reciprocal Inequality: $\frac{1}{a} < b \leftrightarrow \frac{1}{b} < a$ for $a, b > 0$
Informal description
For any positive real numbers $a$ and $b$, the inequality $\frac{1}{a} < b$ holds if and only if $\frac{1}{b} < a$.
le_one_div theorem
(ha : 0 < a) (hb : 0 < b) : a ≤ 1 / b ↔ b ≤ 1 / a
Full source 
theorem le_one_div (ha : 0 < a) (hb : 0 < b) : a ≤ 1 / b ↔ b ≤ 1 / a := by
  simpa using le_inv_comm₀ ha hb
Order Reversal of Reciprocals: $a \leq 1/b \leftrightarrow b \leq 1/a$ for $a, b > 0$
Informal description
For any positive elements $a$ and $b$ in a linearly ordered field, the inequality $a \leq 1/b$ holds if and only if $b \leq 1/a$.
lt_one_div theorem
(ha : 0 < a) (hb : 0 < b) : a < 1 / b ↔ b < 1 / a
Full source 
theorem lt_one_div (ha : 0 < a) (hb : 0 < b) : a < 1 / b ↔ b < 1 / a := by
  simpa using lt_inv_comm₀ ha hb
Reciprocal Inequality: $a < \frac{1}{b} \leftrightarrow b < \frac{1}{a}$ for $a, b > 0$
Informal description
For any positive elements $a$ and $b$ in a linearly ordered field, the inequality $a < \frac{1}{b}$ holds if and only if $b < \frac{1}{a}$.
Bound.one_lt_div_of_pos_of_lt theorem
(b0 : 0 < b) : b < a → 1 < a / b
Full source 
@[bound] lemma Bound.one_lt_div_of_pos_of_lt (b0 : 0 < b) : b < a → 1 < a / b := (one_lt_div b0).mpr
Inequality implication: $b < a \Rightarrow 1 < a/b$ for $b > 0$
Informal description
For any elements $a$ and $b$ in a linearly ordered field, if $0 < b$ and $b < a$, then $1 < a / b$.
Bound.div_lt_one_of_pos_of_lt theorem
(b0 : 0 < b) : a < b → a / b < 1
Full source 
@[bound] lemma Bound.div_lt_one_of_pos_of_lt (b0 : 0 < b) : a < b → a / b < 1 := (div_lt_one b0).mpr
Division by Positive Number Preserves Inequality: $a < b \Rightarrow \frac{a}{b} < 1$
Informal description
For any positive real number $b > 0$, if $a < b$, then $\frac{a}{b} < 1$.
one_div_le_one_div_of_le theorem
(ha : 0 < a) (h : a ≤ b) : 1 / b ≤ 1 / a
Full source 
theorem one_div_le_one_div_of_le (ha : 0 < a) (h : a ≤ b) : 1 / b ≤ 1 / a := by
  simpa using inv_anti₀ ha h
Reciprocal Inequality for Positive Numbers: $a \leq b \Rightarrow \frac{1}{b} \leq \frac{1}{a}$ when $a > 0$
Informal description
For any positive real numbers $a$ and $b$ such that $0 < a \leq b$, the inequality $\frac{1}{b} \leq \frac{1}{a}$ holds.
one_div_lt_one_div_of_lt theorem
(ha : 0 < a) (h : a < b) : 1 / b < 1 / a
Full source 
theorem one_div_lt_one_div_of_lt (ha : 0 < a) (h : a < b) : 1 / b < 1 / a := by
  rwa [lt_div_iff₀' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)]
Reciprocal Inequality for Positive Numbers: $\frac{1}{b} < \frac{1}{a}$ when $0 < a < b$
Informal description
For any positive real numbers $a$ and $b$ such that $0 < a < b$, the inequality $\frac{1}{b} < \frac{1}{a}$ holds.
le_of_one_div_le_one_div theorem
(ha : 0 < a) (h : 1 / a ≤ 1 / b) : b ≤ a
Full source 
theorem le_of_one_div_le_one_div (ha : 0 < a) (h : 1 / a ≤ 1 / b) : b ≤ a :=
  le_imp_le_of_lt_imp_lt (one_div_lt_one_div_of_lt ha) h
Inequality Reversal for Reciprocals of Positive Numbers
Informal description
For any positive real numbers $a$ and $b$, if $\frac{1}{a} \leq \frac{1}{b}$, then $b \leq a$.
lt_of_one_div_lt_one_div theorem
(ha : 0 < a) (h : 1 / a < 1 / b) : b < a
Full source 
theorem lt_of_one_div_lt_one_div (ha : 0 < a) (h : 1 / a < 1 / b) : b < a :=
  lt_imp_lt_of_le_imp_le (one_div_le_one_div_of_le ha) h
Strict Inequality Reversal for Reciprocals of Positive Numbers
Informal description
For any positive real numbers $a$ and $b$, if $\frac{1}{a} < \frac{1}{b}$, then $b < a$.
one_div_le_one_div theorem
(ha : 0 < a) (hb : 0 < b) : 1 / a ≤ 1 / b ↔ b ≤ a
Full source 
/-- For the single implications with fewer assumptions, see `one_div_le_one_div_of_le` and
  `le_of_one_div_le_one_div` -/
theorem one_div_le_one_div (ha : 0 < a) (hb : 0 < b) : 1 / a ≤ 1 / b ↔ b ≤ a :=
  div_le_div_iff_of_pos_left zero_lt_one ha hb
Reciprocal Inequality: $\frac{1}{a} \leq \frac{1}{b} \leftrightarrow b \leq a$ for $a, b > 0$
Informal description
For any positive real numbers $a$ and $b$, the inequality $\frac{1}{a} \leq \frac{1}{b}$ holds if and only if $b \leq a$.
one_div_lt_one_div theorem
(ha : 0 < a) (hb : 0 < b) : 1 / a < 1 / b ↔ b < a
Full source 
/-- For the single implications with fewer assumptions, see `one_div_lt_one_div_of_lt` and
  `lt_of_one_div_lt_one_div` -/
theorem one_div_lt_one_div (ha : 0 < a) (hb : 0 < b) : 1 / a < 1 / b ↔ b < a :=
  div_lt_div_iff_of_pos_left zero_lt_one ha hb
Reciprocal Inequality: $\frac{1}{a} < \frac{1}{b} \leftrightarrow b < a$ for $a, b > 0$
Informal description
For any positive real numbers $a$ and $b$, the inequality $\frac{1}{a} < \frac{1}{b}$ holds if and only if $b < a$.
one_lt_one_div theorem
(h1 : 0 < a) (h2 : a < 1) : 1 < 1 / a
Full source 
theorem one_lt_one_div (h1 : 0 < a) (h2 : a < 1) : 1 < 1 / a := by
  rwa [lt_one_div (@zero_lt_one α _ _ _ _ _) h1, one_div_one]
Reciprocal Inequality: $1 < \frac{1}{a}$ for $0 < a < 1$
Informal description
For any positive element $a$ in a linearly ordered field, if $a < 1$, then $1 < \frac{1}{a}$.
one_le_one_div theorem
(h1 : 0 < a) (h2 : a ≤ 1) : 1 ≤ 1 / a
Full source 
theorem one_le_one_div (h1 : 0 < a) (h2 : a ≤ 1) : 1 ≤ 1 / a := by
  rwa [le_one_div (@zero_lt_one α _ _ _ _ _) h1, one_div_one]
Reciprocal Inequality: $1 \leq \frac{1}{a}$ for $0 < a \leq 1$
Informal description
For any positive element $a$ in a linearly ordered field, if $0 < a \leq 1$, then $1 \leq \frac{1}{a}$.
half_pos theorem
(h : 0 < a) : 0 < a / 2
Full source 
theorem half_pos (h : 0 < a) : 0 < a / 2 :=
  div_pos h zero_lt_two
Positivity of Half: $0 < a / 2$ when $0 < a$
Informal description
For any element $a$ in a linear ordered field, if $0 < a$, then $0 < a / 2$.
one_half_pos theorem
: (0 : α) < 1 / 2
Full source 
theorem one_half_pos : (0 : α) < 1 / 2 :=
  half_pos zero_lt_one
Positivity of One Half: $0 < \frac{1}{2}$
Informal description
In any linear ordered field $\alpha$, the element $\frac{1}{2}$ is strictly positive, i.e., $0 < \frac{1}{2}$.
one_half_lt_one theorem
: (1 / 2 : α) < 1
Full source 
theorem one_half_lt_one : (1 / 2 : α) < 1 :=
  half_lt_self zero_lt_one
Inequality $\frac{1}{2} < 1$ in ordered fields
Informal description
In any linearly ordered field $\alpha$, the inequality $\frac{1}{2} < 1$ holds.
two_inv_lt_one theorem
: (2⁻¹ : α) < 1
Full source 
theorem two_inv_lt_one : (2⁻¹ : α) < 1 :=
  (one_div _).symm.trans_lt one_half_lt_one
Inequality $2^{-1} < 1$ in ordered fields
Informal description
In any linearly ordered field $\alpha$, the inequality $2^{-1} < 1$ holds.
left_lt_add_div_two theorem
: a < (a + b) / 2 ↔ a < b
Full source 
theorem left_lt_add_div_two : a < (a + b) / 2 ↔ a < b := by simp [lt_div_iff₀, mul_two]
Inequality Characterization via Midpoint: $a < \frac{a+b}{2} \leftrightarrow a < b$
Informal description
For any elements $a$ and $b$ in a linearly ordered field $\alpha$, the inequality $a < \frac{a + b}{2}$ holds if and only if $a < b$.
add_div_two_lt_right theorem
: (a + b) / 2 < b ↔ a < b
Full source 
theorem add_div_two_lt_right : (a + b) / 2 < b ↔ a < b := by simp [div_lt_iff₀, mul_two]
Average Less Than Right Endpoint: $\frac{a + b}{2} < b \leftrightarrow a < b$
Informal description
For any elements $a$ and $b$ in a linearly ordered field, the average $(a + b)/2$ is less than $b$ if and only if $a$ is less than $b$, i.e., \[ \frac{a + b}{2} < b \leftrightarrow a < b. \]
add_thirds theorem
(a : α) : a / 3 + a / 3 + a / 3 = a
Full source 
theorem add_thirds (a : α) : a / 3 + a / 3 + a / 3 = a := by
  rw [div_add_div_same, div_add_div_same, ← two_mul, ← add_one_mul 2 a, two_add_one_eq_three,
    mul_div_cancel_left₀ a three_ne_zero]
Sum of Thirds Equals Original: $\frac{a}{3} + \frac{a}{3} + \frac{a}{3} = a$
Informal description
For any element $a$ in a linearly ordered field $\alpha$, the sum of three equal parts of $a$ (each being $a/3$) equals $a$ itself, i.e., \[ \frac{a}{3} + \frac{a}{3} + \frac{a}{3} = a. \]
div_pos_iff_of_pos_left theorem
(ha : 0 < a) : 0 < a / b ↔ 0 < b
Full source 
@[simp] lemma div_pos_iff_of_pos_left (ha : 0 < a) : 0 < a / b ↔ 0 < b := by
  simp only [div_eq_mul_inv, mul_pos_iff_of_pos_left ha, inv_pos]
Positivity of Quotient under Positive Numerator: $\frac{a}{b} > 0 \leftrightarrow b > 0$ when $a > 0$
Informal description
For any elements $a$ and $b$ in a linearly ordered field, if $a > 0$, then the quotient $a / b$ is positive if and only if $b$ is positive, i.e., \[ \frac{a}{b} > 0 \leftrightarrow b > 0. \]
div_pos_iff_of_pos_right theorem
(hb : 0 < b) : 0 < a / b ↔ 0 < a
Full source 
@[simp] lemma div_pos_iff_of_pos_right (hb : 0 < b) : 0 < a / b ↔ 0 < a := by
  simp only [div_eq_mul_inv, mul_pos_iff_of_pos_right (inv_pos.2 hb)]
Positivity of Quotient under Positive Denominator: $b > 0 \implies (a/b > 0 \leftrightarrow a > 0)$
Informal description
For any elements $a$ and $b$ in a linearly ordered field where $b > 0$, the quotient $a/b$ is positive if and only if $a$ is positive, i.e., $0 < a/b \leftrightarrow 0 < a$.
mul_le_mul_of_mul_div_le theorem
(h : a * (b / c) ≤ d) (hc : 0 < c) : b * a ≤ d * c
Full source 
theorem mul_le_mul_of_mul_div_le (h : a * (b / c) ≤ d) (hc : 0 < c) : b * a ≤ d * c := by
  rw [← mul_div_assoc] at h
  rwa [mul_comm b, ← div_le_iff₀ hc]
Inequality Transformation via Division: $a \cdot (b/c) \leq d \implies b \cdot a \leq d \cdot c$ for $c > 0$
Informal description
For any elements $a, b, c, d$ in a linearly ordered field, if $a \cdot (b / c) \leq d$ and $c > 0$, then $b \cdot a \leq d \cdot c$.
div_mul_le_div_mul_of_div_le_div theorem
(h : a / b ≤ c / d) (he : 0 ≤ e) : a / (b * e) ≤ c / (d * e)
Full source 
theorem div_mul_le_div_mul_of_div_le_div (h : a / b ≤ c / d) (he : 0 ≤ e) :
    a / (b * e) ≤ c / (d * e) := by
  rw [div_mul_eq_div_mul_one_div, div_mul_eq_div_mul_one_div]
  exact mul_le_mul_of_nonneg_right h (one_div_nonneg.2 he)
Inequality Preservation Under Multiplication of Denominator: $a/b \leq c/d \implies a/(be) \leq c/(de)$ for $e \geq 0$
Informal description
For any elements $a, b, c, d, e$ in a linearly ordered field, if $a/b \leq c/d$ and $e \geq 0$, then $a/(b \cdot e) \leq c/(d \cdot e)$.
exists_pos_mul_lt theorem
{a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b * c < a
Full source 
theorem exists_pos_mul_lt {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b * c < a := by
  have : 0 < a / max (b + 1) 1 := div_pos h (lt_max_iff.2 (Or.inr zero_lt_one))
  refine ⟨a / max (b + 1) 1, this, ?_⟩
  rw [← lt_div_iff₀ this, div_div_cancel₀ h.ne']
  exact lt_max_iff.2 (Or.inl <| lt_add_one _)
Existence of Positive Scalar Making Product Less Than Given Positive Value
Informal description
For any element $a > 0$ in a linearly ordered field $\alpha$ and any element $b \in \alpha$, there exists an element $c > 0$ such that $b \cdot c < a$.
exists_pos_lt_mul theorem
{a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b < c * a
Full source 
theorem exists_pos_lt_mul {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b < c * a :=
  let ⟨c, hc₀, hc⟩ := exists_pos_mul_lt h b;
  ⟨c⁻¹, inv_pos.2 hc₀, by rwa [← div_eq_inv_mul, lt_div_iff₀ hc₀]⟩
Existence of Positive Scalar Making Product Exceed Given Value
Informal description
For any positive element $a$ in a linearly ordered field $\alpha$ and any element $b \in \alpha$, there exists a positive element $c$ such that $b < c \cdot a$.
monotone_div_right_of_nonneg theorem
(ha : 0 ≤ a) : Monotone (· / a)
Full source 
lemma monotone_div_right_of_nonneg (ha : 0 ≤ a) : Monotone (· / a) :=
  fun _b _c hbc ↦ div_le_div_of_nonneg_right hbc ha
Monotonicity of Right Division by Nonnegative Elements
Informal description
For any element $a$ in a preordered division monoid such that $a \geq 0$, the function $x \mapsto x / a$ is monotone. That is, for any $x \leq y$, we have $x / a \leq y / a$.
strictMono_div_right_of_pos theorem
(ha : 0 < a) : StrictMono (· / a)
Full source 
lemma strictMono_div_right_of_pos (ha : 0 < a) : StrictMono (· / a) :=
  fun _b _c hbc ↦ div_lt_div_of_pos_right hbc ha
Strict Monotonicity of Right Division by Positive Elements: $x \mapsto x/a$ is strictly increasing for $a > 0$
Informal description
For any positive element $a$ in a linearly ordered semifield (i.e., $0 < a$), the function $x \mapsto x / a$ is strictly increasing. That is, for any $x_1, x_2$ in the semifield, if $x_1 < x_2$, then $x_1 / a < x_2 / a$.
Monotone.div_const theorem
{β : Type*} [Preorder β] {f : β → α} (hf : Monotone f) {c : α} (hc : 0 ≤ c) : Monotone fun x => f x / c
Full source 
theorem Monotone.div_const {β : Type*} [Preorder β] {f : β → α} (hf : Monotone f) {c : α}
    (hc : 0 ≤ c) : Monotone fun x => f x / c := (monotone_div_right_of_nonneg hc).comp hf
Monotonicity of Division by Nonnegative Constant: $x \mapsto f(x)/c$ is monotone for $c \geq 0$
Informal description
Let $\alpha$ be a linearly ordered semifield and $\beta$ a preordered type. If $f : \beta \to \alpha$ is a monotone function and $c \in \alpha$ is a nonnegative element (i.e., $0 \leq c$), then the function $x \mapsto f(x) / c$ is also monotone. That is, for any $x_1, x_2 \in \beta$ with $x_1 \leq x_2$, we have $f(x_1) / c \leq f(x_2) / c$.
StrictMono.div_const theorem
{β : Type*} [Preorder β] {f : β → α} (hf : StrictMono f) {c : α} (hc : 0 < c) : StrictMono fun x => f x / c
Full source 
theorem StrictMono.div_const {β : Type*} [Preorder β] {f : β → α} (hf : StrictMono f) {c : α}
    (hc : 0 < c) : StrictMono fun x => f x / c := by
  simpa only [div_eq_mul_inv] using hf.mul_const (inv_pos.2 hc)
Strictly Increasing Function Divided by Positive Constant is Strictly Increasing
Informal description
Let $\alpha$ be a linearly ordered semifield, $\beta$ a preordered type, and $f : \beta \to \alpha$ a strictly increasing function. For any positive element $c \in \alpha$ (i.e., $0 < c$), the function $x \mapsto f(x) / c$ is strictly increasing.
LinearOrderedSemiField.toDenselyOrdered instance
: DenselyOrdered α
Full source 
instance (priority := 100) LinearOrderedSemiField.toDenselyOrdered : DenselyOrdered α where
  dense a₁ a₂ h :=
    ⟨(a₁ + a₂) / 2,
      calc
        a₁ = (a₁ + a₁) / 2 := (add_self_div_two a₁).symm
        _ < (a₁ + a₂) / 2 := div_lt_div_of_pos_right (add_lt_add_left h _) zero_lt_two
        ,
      calc
        (a₁ + a₂) / 2 < (a₂ + a₂) / 2 := div_lt_div_of_pos_right (add_lt_add_right h _) zero_lt_two
        _ = a₂ := add_self_div_two a₂
        ⟩
Dense Order Property of Linearly Ordered Semifields
Informal description
Every linearly ordered semifield $\alpha$ is densely ordered. That is, for any two elements $a, b \in \alpha$ with $a < b$, there exists an element $c \in \alpha$ such that $a < c < b$.
min_div_div_right theorem
{c : α} (hc : 0 ≤ c) (a b : α) : min (a / c) (b / c) = min a b / c
Full source 
theorem min_div_div_right {c : α} (hc : 0 ≤ c) (a b : α) : min (a / c) (b / c) = min a b / c :=
  (monotone_div_right_of_nonneg hc).map_min.symm
Minimum of Ratios Equals Ratio of Minimums for Nonnegative Denominator
Informal description
For any nonnegative element $c$ in a linearly ordered semifield $\alpha$ (i.e., $0 \leq c$), and for any elements $a, b \in \alpha$, the minimum of $a/c$ and $b/c$ equals the minimum of $a$ and $b$ divided by $c$. That is, \[ \min\left(\frac{a}{c}, \frac{b}{c}\right) = \frac{\min(a, b)}{c}. \]
max_div_div_right theorem
{c : α} (hc : 0 ≤ c) (a b : α) : max (a / c) (b / c) = max a b / c
Full source 
theorem max_div_div_right {c : α} (hc : 0 ≤ c) (a b : α) : max (a / c) (b / c) = max a b / c :=
  (monotone_div_right_of_nonneg hc).map_max.symm
Maximum Preserved Under Division by Nonnegative Element: $\max(a/c, b/c) = \max(a, b)/c$
Informal description
For any nonnegative element $c$ in a linearly ordered semifield $\alpha$ (i.e., $c \geq 0$) and any elements $a, b \in \alpha$, the maximum of the divisions $a/c$ and $b/c$ equals the division of the maximum of $a$ and $b$ by $c$, i.e., \[ \max\left(\frac{a}{c}, \frac{b}{c}\right) = \frac{\max(a, b)}{c}. \]
one_div_strictAntiOn theorem
: StrictAntiOn (fun x : α => 1 / x) (Set.Ioi 0)
Full source 
theorem one_div_strictAntiOn : StrictAntiOn (fun x : α => 1 / x) (Set.Ioi 0) :=
  fun _ x1 _ y1 xy => (one_div_lt_one_div (Set.mem_Ioi.mp y1) (Set.mem_Ioi.mp x1)).mpr xy
Strict Antitonicity of Reciprocal Function on Positive Reals: $\frac{1}{y} < \frac{1}{x}$ for $0 < x < y$
Informal description
The function $x \mapsto \frac{1}{x}$ is strictly antitone on the interval $(0, \infty)$. That is, for any $x, y \in (0, \infty)$, if $x < y$ then $\frac{1}{y} < \frac{1}{x}$.
one_div_pow_le_one_div_pow_of_le theorem
(a1 : 1 ≤ a) {m n : ℕ} (mn : m ≤ n) : 1 / a ^ n ≤ 1 / a ^ m
Full source 
theorem one_div_pow_le_one_div_pow_of_le (a1 : 1 ≤ a) {m n : ℕ} (mn : m ≤ n) :
    1 / a ^ n ≤ 1 / a ^ m := by
  refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ a1 mn) <;>
    exact pow_pos (zero_lt_one.trans_le a1) _
Monotonicity of reciprocal powers: $\frac{1}{a^n} \leq \frac{1}{a^m}$ for $a \geq 1$ and $m \leq n$
Informal description
For any real number $a \geq 1$ and natural numbers $m \leq n$, the inequality $\frac{1}{a^n} \leq \frac{1}{a^m}$ holds.
one_div_pow_lt_one_div_pow_of_lt theorem
(a1 : 1 < a) {m n : ℕ} (mn : m < n) : 1 / a ^ n < 1 / a ^ m
Full source 
theorem one_div_pow_lt_one_div_pow_of_lt (a1 : 1 < a) {m n : ℕ} (mn : m < n) :
    1 / a ^ n < 1 / a ^ m := by
  refine (one_div_lt_one_div ?_ ?_).2 (pow_lt_pow_right₀ a1 mn) <;>
    exact pow_pos (zero_lt_one.trans a1) _
Strict Monotonicity of Reciprocal Powers: $\frac{1}{a^n} < \frac{1}{a^m}$ for $a > 1$ and $m < n$
Informal description
For any real number $a > 1$ and natural numbers $m < n$, the inequality $\frac{1}{a^n} < \frac{1}{a^m}$ holds.
one_div_pow_anti theorem
(a1 : 1 ≤ a) : Antitone fun n : ℕ => 1 / a ^ n
Full source 
theorem one_div_pow_anti (a1 : 1 ≤ a) : Antitone fun n : ℕ => 1 / a ^ n := fun _ _ =>
  one_div_pow_le_one_div_pow_of_le a1
Antitonicity of Reciprocal Powers for $a \geq 1$
Informal description
For any real number $a \geq 1$, the function $n \mapsto \frac{1}{a^n}$ is antitone on the natural numbers. That is, for any natural numbers $m \leq n$, we have $\frac{1}{a^n} \leq \frac{1}{a^m}$.
one_div_pow_strictAnti theorem
(a1 : 1 < a) : StrictAnti fun n : ℕ => 1 / a ^ n
Full source 
theorem one_div_pow_strictAnti (a1 : 1 < a) : StrictAnti fun n : ℕ => 1 / a ^ n := fun _ _ =>
  one_div_pow_lt_one_div_pow_of_lt a1
Strict Antitonicity of $\frac{1}{a^n}$ for $a > 1$
Informal description
For any real number $a > 1$, the function $n \mapsto \frac{1}{a^n}$ is strictly antitone on the natural numbers. That is, for any natural numbers $m < n$, we have $\frac{1}{a^n} < \frac{1}{a^m}$.
inv_strictAntiOn theorem
: StrictAntiOn (fun x : α => x⁻¹) (Set.Ioi 0)
Full source 
theorem inv_strictAntiOn : StrictAntiOn (fun x : α => x⁻¹) (Set.Ioi 0) := fun _ hx _ hy xy =>
  (inv_lt_inv₀ hy hx).2 xy
Strict Antitonicity of Inverse Function on Positive Reals
Informal description
The function $x \mapsto x^{-1}$ is strictly antitone on the interval $(0, \infty)$ in a linearly ordered field $\alpha$. That is, for any $x, y \in (0, \infty)$, if $x < y$ then $y^{-1} < x^{-1}$.
inv_pow_le_inv_pow_of_le theorem
(a1 : 1 ≤ a) {m n : ℕ} (mn : m ≤ n) : (a ^ n)⁻¹ ≤ (a ^ m)⁻¹
Full source 
theorem inv_pow_le_inv_pow_of_le (a1 : 1 ≤ a) {m n : ℕ} (mn : m ≤ n) : (a ^ n)⁻¹ ≤ (a ^ m)⁻¹ := by
  convert one_div_pow_le_one_div_pow_of_le a1 mn using 1 <;> simp
Monotonicity of inverse powers: $(a^n)^{-1} \leq (a^m)^{-1}$ for $a \geq 1$ and $m \leq n$
Informal description
For any real number $a \geq 1$ and natural numbers $m \leq n$, the inequality $(a^n)^{-1} \leq (a^m)^{-1}$ holds.
inv_pow_lt_inv_pow_of_lt theorem
(a1 : 1 < a) {m n : ℕ} (mn : m < n) : (a ^ n)⁻¹ < (a ^ m)⁻¹
Full source 
theorem inv_pow_lt_inv_pow_of_lt (a1 : 1 < a) {m n : ℕ} (mn : m < n) : (a ^ n)⁻¹ < (a ^ m)⁻¹ := by
  convert one_div_pow_lt_one_div_pow_of_lt a1 mn using 1 <;> simp
Strict Monotonicity of Inverse Powers: $(a^n)^{-1} < (a^m)^{-1}$ for $a > 1$ and $m < n$
Informal description
For any real number $a > 1$ and natural numbers $m < n$, the inequality $(a^n)^{-1} < (a^m)^{-1}$ holds.
inv_pow_anti theorem
(a1 : 1 ≤ a) : Antitone fun n : ℕ => (a ^ n)⁻¹
Full source 
theorem inv_pow_anti (a1 : 1 ≤ a) : Antitone fun n : ℕ => (a ^ n)⁻¹ := fun _ _ =>
  inv_pow_le_inv_pow_of_le a1
Antitonicity of inverse powers for $a \geq 1$
Informal description
For any real number $a \geq 1$, the function $n \mapsto (a^n)^{-1}$ is antitone on the natural numbers, meaning that for any $m, n \in \mathbb{N}$ with $m \leq n$, we have $(a^n)^{-1} \leq (a^m)^{-1}$.
inv_pow_strictAnti theorem
(a1 : 1 < a) : StrictAnti fun n : ℕ => (a ^ n)⁻¹
Full source 
theorem inv_pow_strictAnti (a1 : 1 < a) : StrictAnti fun n : ℕ => (a ^ n)⁻¹ := fun _ _ =>
  inv_pow_lt_inv_pow_of_lt a1
Strict Antitonicity of Inverse Powers: $(a^n)^{-1} < (a^m)^{-1}$ for $a > 1$ and $m < n$
Informal description
For any real number $a > 1$, the function $n \mapsto (a^n)^{-1}$ is strictly antitone on the natural numbers, meaning that for any $m, n \in \mathbb{N}$ with $m < n$, we have $(a^n)^{-1} < (a^m)^{-1}$.
le_iff_forall_one_lt_le_mul₀ theorem
{α : Type*} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (hb : 0 ≤ b) : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε
Full source 
theorem le_iff_forall_one_lt_le_mul₀ {α : Type*}
    [Semifield α] [LinearOrder α] [IsStrictOrderedRing α]
    {a b : α} (hb : 0 ≤ b) : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε := by
  refine ⟨fun h _ hε ↦ h.trans <| le_mul_of_one_le_right hb hε.le, fun h ↦ ?_⟩
  obtain rfl|hb := hb.eq_or_lt
  · simp_rw [zero_mul] at h
    exact h 2 one_lt_two
  refine le_of_forall_gt_imp_ge_of_dense fun x hbx => ?_
  convert h (x / b) ((one_lt_div hb).mpr hbx)
  rw [mul_div_cancel₀ _ hb.ne']
Characterization of Inequality via Multiplicative Perturbations: $a \leq b \leftrightarrow \forall \varepsilon > 1, a \leq b \cdot \varepsilon$
Informal description
Let $\alpha$ be a linearly ordered semifield that is also a strict ordered ring. For any elements $a, b \in \alpha$ with $b \geq 0$, we have $a \leq b$ if and only if for every $\varepsilon > 1$, the inequality $a \leq b \cdot \varepsilon$ holds.
IsGLB.mul_left theorem
{s : Set α} (ha : 0 ≤ a) (hs : IsGLB s b) : IsGLB ((fun b => a * b) '' s) (a * b)
Full source 
theorem IsGLB.mul_left {s : Set α} (ha : 0 ≤ a) (hs : IsGLB s b) :
    IsGLB ((fun b => a * b) '' s) (a * b) := by
  rcases lt_or_eq_of_le ha with (ha | rfl)
  · exact (OrderIso.mulLeft₀ _ ha).isGLB_image'.2 hs
  · simp_rw [zero_mul]
    rw [hs.nonempty.image_const]
    exact isGLB_singleton
Infimum Preservation under Left Multiplication by Nonnegative Elements: $\text{inf}(a \cdot s) = a \cdot \text{inf}(s)$
Informal description
Let $\alpha$ be a linearly ordered semifield, and let $s$ be a subset of $\alpha$ with greatest lower bound $b$. For any nonnegative element $a \in \alpha$ (i.e., $0 \leq a$), the image of $s$ under left multiplication by $a$ has $a \cdot b$ as its greatest lower bound. In other words, if $b$ is the infimum of $s$, then $a \cdot b$ is the infimum of $\{a \cdot x \mid x \in s\}$.
IsGLB.mul_right theorem
{s : Set α} (ha : 0 ≤ a) (hs : IsGLB s b) : IsGLB ((fun b => b * a) '' s) (b * a)
Full source 
theorem IsGLB.mul_right {s : Set α} (ha : 0 ≤ a) (hs : IsGLB s b) :
    IsGLB ((fun b => b * a) '' s) (b * a) := by simpa [mul_comm] using hs.mul_left ha
Infimum Preservation under Right Multiplication by Nonnegative Elements: $\text{inf}(s \cdot a) = \text{inf}(s) \cdot a$
Informal description
Let $\alpha$ be a linearly ordered semifield, and let $s$ be a subset of $\alpha$ with greatest lower bound $b$. For any nonnegative element $a \in \alpha$ (i.e., $0 \leq a$), the image of $s$ under right multiplication by $a$ has $b \cdot a$ as its greatest lower bound. In other words, if $b$ is the infimum of $s$, then $b \cdot a$ is the infimum of $\{x \cdot a \mid x \in s\}$.
div_pos_iff theorem
: 0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
Full source 
theorem div_pos_iff : 0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 := by
  simp only [division_def, mul_pos_iff, inv_pos, inv_lt_zero]
Positivity of Quotient in Ordered Fields: $0 < a/b \iff (0 < a \land 0 < b) \lor (a < 0 \land b < 0)$
Informal description
For any elements $a$ and $b$ in a linearly ordered field, the quotient $a / b$ is positive if and only if either both $a$ and $b$ are positive or both $a$ and $b$ are negative. That is, $$ 0 < \frac{a}{b} \iff (0 < a \land 0 < b) \lor (a < 0 \land b < 0). $$
div_neg_iff theorem
: a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Full source 
theorem div_neg_iff : a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b := by
  simp [division_def, mul_neg_iff]
Quotient Negativity Criterion in Ordered Fields: $\frac{a}{b} < 0 \leftrightarrow (0 < a \land b < 0) \lor (a < 0 \land 0 < b)$
Informal description
For any elements $a$ and $b$ in a linearly ordered field, the quotient $a/b$ is negative if and only if either $a$ is positive and $b$ is negative, or $a$ is negative and $b$ is positive. That is, \[ \frac{a}{b} < 0 \leftrightarrow (0 < a \land b < 0) \lor (a < 0 \land 0 < b). \]
div_nonneg_iff theorem
: 0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
Full source 
theorem div_nonneg_iff : 0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := by
  simp [division_def, mul_nonneg_iff]
Nonnegativity of Quotient in Linearly Ordered Fields
Informal description
For any elements $a$ and $b$ in a linearly ordered field, the quotient $a/b$ is nonnegative if and only if either both $a$ and $b$ are nonnegative or both $a$ and $b$ are nonpositive. In other words: \[ 0 \leq \frac{a}{b} \iff (0 \leq a \land 0 \leq b) \lor (a \leq 0 \land b \leq 0) \]
div_nonpos_iff theorem
: a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Full source 
theorem div_nonpos_iff : a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b := by
  simp [division_def, mul_nonpos_iff]
Nonpositivity of Quotient in Linearly Ordered Fields
Informal description
For any elements $a$ and $b$ in a linearly ordered field, the quotient $a / b$ is nonpositive (i.e., $a / b \leq 0$) if and only if either both $a$ is nonnegative and $b$ is nonpositive, or both $a$ is nonpositive and $b$ is nonnegative. In other words: \[ \frac{a}{b} \leq 0 \iff (0 \leq a \land b \leq 0) \lor (a \leq 0 \land 0 \leq b). \]
div_nonneg_of_nonpos theorem
(ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a / b
Full source 
theorem div_nonneg_of_nonpos (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a / b :=
  div_nonneg_iff.2 <| Or.inr ⟨ha, hb⟩
Nonnegativity of Quotient for Nonpositive Elements in Ordered Fields
Informal description
For any elements $a$ and $b$ in a linearly ordered field, if $a \leq 0$ and $b \leq 0$, then the quotient $a/b$ is nonnegative, i.e., $0 \leq a/b$.
div_pos_of_neg_of_neg theorem
(ha : a < 0) (hb : b < 0) : 0 < a / b
Full source 
theorem div_pos_of_neg_of_neg (ha : a < 0) (hb : b < 0) : 0 < a / b :=
  div_pos_iff.2 <| Or.inr ⟨ha, hb⟩
Positivity of Quotient of Negative Elements: $a < 0 \land b < 0 \implies 0 < a/b$
Informal description
For any elements $a$ and $b$ in a linearly ordered field, if $a < 0$ and $b < 0$, then the quotient $a / b$ is positive, i.e., $0 < a / b$.
div_neg_of_neg_of_pos theorem
(ha : a < 0) (hb : 0 < b) : a / b < 0
Full source 
theorem div_neg_of_neg_of_pos (ha : a < 0) (hb : 0 < b) : a / b < 0 :=
  div_neg_iff.2 <| Or.inr ⟨ha, hb⟩
Negative Divided by Positive is Negative: $\frac{a}{b} < 0$ when $a < 0$ and $0 < b$
Informal description
For any elements $a$ and $b$ in a linearly ordered field, if $a$ is negative and $b$ is positive, then their quotient $a/b$ is negative, i.e., \[ a < 0 \land 0 < b \implies \frac{a}{b} < 0. \]
div_neg_of_pos_of_neg theorem
(ha : 0 < a) (hb : b < 0) : a / b < 0
Full source 
theorem div_neg_of_pos_of_neg (ha : 0 < a) (hb : b < 0) : a / b < 0 :=
  div_neg_iff.2 <| Or.inl ⟨ha, hb⟩
Quotient Negativity for Positive Divided by Negative: $0 < a \land b < 0 \to a/b < 0$
Informal description
For any elements $a$ and $b$ in a linearly ordered field, if $a$ is positive and $b$ is negative, then their quotient $a/b$ is negative, i.e., $a/b < 0$.
div_le_iff_of_neg theorem
(hc : c < 0) : b / c ≤ a ↔ a * c ≤ b
Full source 
theorem div_le_iff_of_neg (hc : c < 0) : b / c ≤ a ↔ a * c ≤ b :=
  ⟨fun h => div_mul_cancel₀ b (ne_of_lt hc) ▸ mul_le_mul_of_nonpos_right h hc.le, fun h =>
    calc
      a = a * c * (1 / c) := mul_mul_div a (ne_of_lt hc)
      _ ≥ b * (1 / c) := mul_le_mul_of_nonpos_right h (one_div_neg.2 hc).le
      _ = b / c := (div_eq_mul_one_div b c).symm
      ⟩
Division Inequality Equivalence for Negative Elements: $\frac{b}{c} \leq a \leftrightarrow a \cdot c \leq b$ when $c < 0$
Informal description
For any negative element $c$ in a linearly ordered field, the inequality $\frac{b}{c} \leq a$ holds if and only if $a \cdot c \leq b$.
div_le_iff_of_neg' theorem
(hc : c < 0) : b / c ≤ a ↔ c * a ≤ b
Full source 
theorem div_le_iff_of_neg' (hc : c < 0) : b / c ≤ a ↔ c * a ≤ b := by
  rw [mul_comm, div_le_iff_of_neg hc]
Division Inequality Equivalence for Negative Elements (Multiplicative Form): $\frac{b}{c} \leq a \leftrightarrow c \cdot a \leq b$ when $c < 0$
Informal description
For any negative element $c$ in a linearly ordered field, the inequality $\frac{b}{c} \leq a$ holds if and only if $c \cdot a \leq b$.
le_div_iff_of_neg theorem
(hc : c < 0) : a ≤ b / c ↔ b ≤ a * c
Full source 
theorem le_div_iff_of_neg (hc : c < 0) : a ≤ b / c ↔ b ≤ a * c := by
  rw [← neg_neg c, mul_neg, div_neg, le_neg, div_le_iff₀ (neg_pos.2 hc), neg_mul]
Division Inequality Equivalence for Negative Elements: $a \leq \frac{b}{c} \leftrightarrow b \leq a \cdot c$ when $c < 0$
Informal description
For any negative element $c$ in a linear ordered field, the inequality $a \leq \frac{b}{c}$ holds if and only if $b \leq a \cdot c$.
le_div_iff_of_neg' theorem
(hc : c < 0) : a ≤ b / c ↔ b ≤ c * a
Full source 
theorem le_div_iff_of_neg' (hc : c < 0) : a ≤ b / c ↔ b ≤ c * a := by
  rw [mul_comm, le_div_iff_of_neg hc]
Division Inequality Equivalence for Negative Elements (Multiplicative Form): $a \leq \frac{b}{c} \leftrightarrow b \leq c \cdot a$ when $c < 0$
Informal description
For any negative element $c$ in a linear ordered field, the inequality $a \leq \frac{b}{c}$ holds if and only if $b \leq c \cdot a$.
div_lt_iff_of_neg theorem
(hc : c < 0) : b / c < a ↔ a * c < b
Full source 
theorem div_lt_iff_of_neg (hc : c < 0) : b / c < a ↔ a * c < b :=
  lt_iff_lt_of_le_iff_le <| le_div_iff_of_neg hc
Division Inequality Equivalence for Negative Elements: $\frac{b}{c} < a \leftrightarrow a \cdot c < b$ when $c < 0$
Informal description
For any element $c < 0$ in a linear ordered field, the inequality $\frac{b}{c} < a$ holds if and only if $a \cdot c < b$.
div_lt_iff_of_neg' theorem
(hc : c < 0) : b / c < a ↔ c * a < b
Full source 
theorem div_lt_iff_of_neg' (hc : c < 0) : b / c < a ↔ c * a < b := by
  rw [mul_comm, div_lt_iff_of_neg hc]
Division Inequality Equivalence for Negative Elements (Multiplicative Form): $\frac{b}{c} < a \leftrightarrow c \cdot a < b$ when $c < 0$
Informal description
For any element $c < 0$ in a linear ordered field, the inequality $\frac{b}{c} < a$ holds if and only if $c \cdot a < b$.
lt_div_iff_of_neg theorem
(hc : c < 0) : a < b / c ↔ b < a * c
Full source 
theorem lt_div_iff_of_neg (hc : c < 0) : a < b / c ↔ b < a * c :=
  lt_iff_lt_of_le_iff_le <| div_le_iff_of_neg hc
Division Inequality Equivalence for Negative Elements: $a < \frac{b}{c} \leftrightarrow b < a \cdot c$ when $c < 0$
Informal description
For any element $c < 0$ in a linearly ordered field, the inequality $a < \frac{b}{c}$ holds if and only if $b < a \cdot c$.
lt_div_iff_of_neg' theorem
(hc : c < 0) : a < b / c ↔ b < c * a
Full source 
theorem lt_div_iff_of_neg' (hc : c < 0) : a < b / c ↔ b < c * a := by
  rw [mul_comm, lt_div_iff_of_neg hc]
Division Inequality Equivalence for Negative Elements (Multiplicative Form): $a < \frac{b}{c} \leftrightarrow b < c \cdot a$ when $c < 0$
Informal description
For any element $c < 0$ in a linearly ordered field, the inequality $a < \frac{b}{c}$ holds if and only if $b < c \cdot a$.
div_le_one_of_ge theorem
(h : b ≤ a) (hb : b ≤ 0) : a / b ≤ 1
Full source 
theorem div_le_one_of_ge (h : b ≤ a) (hb : b ≤ 0) : a / b ≤ 1 := by
  simpa only [neg_div_neg_eq] using div_le_one_of_le₀ (neg_le_neg h) (neg_nonneg_of_nonpos hb)
Division Inequality: $a/b \leq 1$ when $b \leq a$ and $b$ nonpositive
Informal description
For any elements $a$ and $b$ in a linearly ordered field, if $b \leq a$ and $b \leq 0$, then $a / b \leq 1$.
inv_le_inv_of_neg theorem
(ha : a < 0) (hb : b < 0) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a
Full source 
theorem inv_le_inv_of_neg (ha : a < 0) (hb : b < 0) : a⁻¹a⁻¹ ≤ b⁻¹ ↔ b ≤ a := by
  rw [← one_div, div_le_iff_of_neg ha, ← div_eq_inv_mul, div_le_iff_of_neg hb, one_mul]
Inverse Inequality for Negative Reals: $a^{-1} \leq b^{-1} \leftrightarrow b \leq a$ when $a, b < 0$
Informal description
For any negative real numbers $a$ and $b$, the inequality $a^{-1} \leq b^{-1}$ holds if and only if $b \leq a$.
inv_lt_inv_of_neg theorem
(ha : a < 0) (hb : b < 0) : a⁻¹ < b⁻¹ ↔ b < a
Full source 
theorem inv_lt_inv_of_neg (ha : a < 0) (hb : b < 0) : a⁻¹a⁻¹ < b⁻¹ ↔ b < a :=
  lt_iff_lt_of_le_iff_le (inv_le_inv_of_neg hb ha)
Strict Inverse Inequality for Negative Reals: $a^{-1} < b^{-1} \leftrightarrow b < a$ when $a, b < 0$
Informal description
For any negative real numbers $a$ and $b$, the inequality $a^{-1} < b^{-1}$ holds if and only if $b < a$.
inv_lt_of_neg theorem
(ha : a < 0) (hb : b < 0) : a⁻¹ < b ↔ b⁻¹ < a
Full source 
theorem inv_lt_of_neg (ha : a < 0) (hb : b < 0) : a⁻¹a⁻¹ < b ↔ b⁻¹ < a :=
  lt_iff_lt_of_le_iff_le (le_inv_of_neg hb ha)
Inverse Inequality for Negative Reals: $a^{-1} < b \leftrightarrow b^{-1} < a$ when $a, b < 0$
Informal description
For any negative real numbers $a$ and $b$, the inequality $a^{-1} < b$ holds if and only if $b^{-1} < a$.
lt_inv_of_neg theorem
(ha : a < 0) (hb : b < 0) : a < b⁻¹ ↔ b < a⁻¹
Full source 
theorem lt_inv_of_neg (ha : a < 0) (hb : b < 0) : a < b⁻¹ ↔ b < a⁻¹ :=
  lt_iff_lt_of_le_iff_le (inv_le_of_neg hb ha)
Inverse Inequality for Negative Reals: $a < b^{-1} \leftrightarrow b < a^{-1}$
Informal description
For any negative real numbers $a$ and $b$, the inequality $a < b^{-1}$ holds if and only if $b < a^{-1}$.
sub_inv_antitoneOn_Ioi theorem
: AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Ioi c)
Full source 
theorem sub_inv_antitoneOn_Ioi :
    AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Ioi c) :=
  antitoneOn_iff_forall_lt.mpr fun _ ha _ hb hab ↦
    inv_le_inv₀ (sub_pos.mpr hb) (sub_pos.mpr ha) |>.mpr <| sub_le_sub (le_of_lt hab) le_rfl
Antitonicity of $(x - c)^{-1}$ on $(c, \infty)$
Informal description
For any real number $c$, the function $f(x) = (x - c)^{-1}$ is antitone on the interval $(c, \infty)$. That is, for any $x, y \in (c, \infty)$, if $x \leq y$, then $(y - c)^{-1} \leq (x - c)^{-1}$.
sub_inv_antitoneOn_Iio theorem
: AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Iio c)
Full source 
theorem sub_inv_antitoneOn_Iio :
    AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Iio c) :=
  antitoneOn_iff_forall_lt.mpr fun _ ha _ hb hab ↦
    inv_le_inv_of_neg (sub_neg.mpr hb) (sub_neg.mpr ha) |>.mpr <| sub_le_sub (le_of_lt hab) le_rfl
Antitonicity of $(x - c)^{-1}$ on $(-\infty, c)$
Informal description
For any real number $c$, the function $f(x) = (x - c)^{-1}$ is antitone on the interval $(-\infty, c)$. That is, for any $x, y \in (-\infty, c)$, if $x \leq y$, then $(y - c)^{-1} \leq (x - c)^{-1}$.
sub_inv_antitoneOn_Icc_right theorem
(ha : c < a) : AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)
Full source 
theorem sub_inv_antitoneOn_Icc_right (ha : c < a) :
    AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Icc a b) := by
  by_cases hab : a ≤ b
  · exact sub_inv_antitoneOn_Ioi.mono <| (Set.Icc_subset_Ioi_iff hab).mpr ha
  · simp [hab, Set.Subsingleton.antitoneOn]
Antitonicity of $(x - c)^{-1}$ on $[a, b]$ when $c < a$
Informal description
For any real numbers $a$, $b$, and $c$ such that $c < a$, the function $f(x) = (x - c)^{-1}$ is antitone on the closed interval $[a, b]$. That is, for any $x, y \in [a, b]$, if $x \leq y$, then $(y - c)^{-1} \leq (x - c)^{-1}$.
sub_inv_antitoneOn_Icc_left theorem
(ha : b < c) : AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)
Full source 
theorem sub_inv_antitoneOn_Icc_left (ha : b < c) :
    AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Icc a b) := by
  by_cases hab : a ≤ b
  · exact sub_inv_antitoneOn_Iio.mono <| (Set.Icc_subset_Iio_iff hab).mpr ha
  · simp [hab, Set.Subsingleton.antitoneOn]
Antitonicity of $(x - c)^{-1}$ on $[a, b]$ when $b < c$
Informal description
For any real numbers $a$, $b$, and $c$ such that $b < c$, the function $f(x) = (x - c)^{-1}$ is antitone on the closed interval $[a, b]$. That is, for any $x, y \in [a, b]$, if $x \leq y$, then $(y - c)^{-1} \leq (x - c)^{-1}$.
inv_antitoneOn_Ioi theorem
: AntitoneOn (fun x : α ↦ x⁻¹) (Set.Ioi 0)
Full source 
theorem inv_antitoneOn_Ioi :
    AntitoneOn (fun x : α ↦ x⁻¹) (Set.Ioi 0) := by
  convert sub_inv_antitoneOn_Ioi (α := α)
  exact (sub_zero _).symm
Antitonicity of $x^{-1}$ on $(0, \infty)$
Informal description
For any element $x$ in the interval $(0, \infty)$, the function $f(x) = x^{-1}$ is antitone. That is, for any $x, y \in (0, \infty)$, if $x \leq y$, then $y^{-1} \leq x^{-1}$.
inv_antitoneOn_Iio theorem
: AntitoneOn (fun x : α ↦ x⁻¹) (Set.Iio 0)
Full source 
theorem inv_antitoneOn_Iio :
    AntitoneOn (fun x : α ↦ x⁻¹) (Set.Iio 0) := by
  convert sub_inv_antitoneOn_Iio (α := α)
  exact (sub_zero _).symm
Antitonicity of $x^{-1}$ on $(-\infty, 0)$
Informal description
The function $f(x) = x^{-1}$ is antitone on the interval $(-\infty, 0)$. That is, for any $x, y \in (-\infty, 0)$, if $x \leq y$, then $y^{-1} \leq x^{-1}$.
inv_antitoneOn_Icc_right theorem
(ha : 0 < a) : AntitoneOn (fun x : α ↦ x⁻¹) (Set.Icc a b)
Full source 
theorem inv_antitoneOn_Icc_right (ha : 0 < a) :
    AntitoneOn (fun x : α ↦ x⁻¹) (Set.Icc a b) := by
  convert sub_inv_antitoneOn_Icc_right ha
  exact (sub_zero _).symm
Antitonicity of $x^{-1}$ on $[a, b]$ for $a > 0$
Informal description
For any elements $a$ and $b$ in a linearly ordered field $\alpha$ with $0 < a$, the function $f(x) = x^{-1}$ is antitone on the closed interval $[a, b]$. That is, for any $x, y \in [a, b]$, if $x \leq y$, then $y^{-1} \leq x^{-1}$.
inv_antitoneOn_Icc_left theorem
(hb : b < 0) : AntitoneOn (fun x : α ↦ x⁻¹) (Set.Icc a b)
Full source 
theorem inv_antitoneOn_Icc_left (hb : b < 0) :
    AntitoneOn (fun x : α ↦ x⁻¹) (Set.Icc a b) := by
  convert sub_inv_antitoneOn_Icc_left hb
  exact (sub_zero _).symm
Antitonicity of $x^{-1}$ on $[a, b]$ for $b < 0$
Informal description
For any elements $a$ and $b$ in a linearly ordered field $\alpha$ with $b < 0$, the function $f(x) = x^{-1}$ is antitone on the closed interval $[a, b]$. That is, for any $x, y \in [a, b]$, if $x \leq y$, then $y^{-1} \leq x^{-1}$.
div_le_div_of_nonpos_of_le theorem
(hc : c ≤ 0) (h : b ≤ a) : a / c ≤ b / c
Full source 
theorem div_le_div_of_nonpos_of_le (hc : c ≤ 0) (h : b ≤ a) : a / c ≤ b / c := by
  rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
  exact mul_le_mul_of_nonpos_right h (one_div_nonpos.2 hc)
Division Inequality for Nonpositive Denominator: $c \leq 0 \implies (b \leq a \to a/c \leq b/c)$
Informal description
For any elements $a, b, c$ in a linearly ordered field, if $c \leq 0$ and $b \leq a$, then $a/c \leq b/c$.
div_lt_div_of_neg_of_lt theorem
(hc : c < 0) (h : b < a) : a / c < b / c
Full source 
theorem div_lt_div_of_neg_of_lt (hc : c < 0) (h : b < a) : a / c < b / c := by
  rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
  exact mul_lt_mul_of_neg_right h (one_div_neg.2 hc)
Division Reversal under Negative Denominator: $c < 0 \implies (b < a \to a/c < b/c)$
Informal description
For any elements $a, b, c$ in a linearly ordered field where $c < 0$ and $b < a$, it holds that $a / c < b / c$.
div_le_div_right_of_neg theorem
(hc : c < 0) : a / c ≤ b / c ↔ b ≤ a
Full source 
theorem div_le_div_right_of_neg (hc : c < 0) : a / c ≤ b / c ↔ b ≤ a :=
  ⟨le_imp_le_of_lt_imp_lt <| div_lt_div_of_neg_of_lt hc, div_le_div_of_nonpos_of_le <| hc.le⟩
Division Inequality Reversal for Negative Denominator: $\frac{a}{c} \leq \frac{b}{c} \leftrightarrow b \leq a$ when $c < 0$
Informal description
For any elements $a, b, c$ in a linearly ordered field with $c < 0$, the inequality $\frac{a}{c} \leq \frac{b}{c}$ holds if and only if $b \leq a$.
div_lt_div_right_of_neg theorem
(hc : c < 0) : a / c < b / c ↔ b < a
Full source 
theorem div_lt_div_right_of_neg (hc : c < 0) : a / c < b / c ↔ b < a :=
  lt_iff_lt_of_le_iff_le <| div_le_div_right_of_neg hc
Strict Division Inequality Reversal for Negative Denominator: $\frac{a}{c} < \frac{b}{c} \leftrightarrow b < a$ when $c < 0$
Informal description
For any elements $a, b, c$ in a linearly ordered field with $c < 0$, the strict inequality $\frac{a}{c} < \frac{b}{c}$ holds if and only if $b < a$.
one_le_div_of_neg theorem
(hb : b < 0) : 1 ≤ a / b ↔ a ≤ b
Full source 
theorem one_le_div_of_neg (hb : b < 0) : 1 ≤ a / b ↔ a ≤ b := by rw [le_div_iff_of_neg hb, one_mul]
Inequality Equivalence for Division by Negative Elements: $1 \leq \frac{a}{b} \leftrightarrow a \leq b$ when $b < 0$
Informal description
For any element $b < 0$ in a linear ordered field, the inequality $1 \leq \frac{a}{b}$ holds if and only if $a \leq b$.
div_le_one_of_neg theorem
(hb : b < 0) : a / b ≤ 1 ↔ b ≤ a
Full source 
theorem div_le_one_of_neg (hb : b < 0) : a / b ≤ 1 ↔ b ≤ a := by rw [div_le_iff_of_neg hb, one_mul]
Division by Negative Element Less Than or Equal to One: $\frac{a}{b} \leq 1 \leftrightarrow b \leq a$ when $b < 0$
Informal description
For any element $b < 0$ in a linearly ordered field, the inequality $\frac{a}{b} \leq 1$ holds if and only if $b \leq a$.
one_lt_div_of_neg theorem
(hb : b < 0) : 1 < a / b ↔ a < b
Full source 
theorem one_lt_div_of_neg (hb : b < 0) : 1 < a / b ↔ a < b := by rw [lt_div_iff_of_neg hb, one_mul]
Inequality Equivalence for Division by Negative Elements: $1 < \frac{a}{b} \leftrightarrow a < b$ when $b < 0$
Informal description
For any element $b < 0$ in a linearly ordered field, the inequality $1 < \frac{a}{b}$ holds if and only if $a < b$.
div_lt_one_of_neg theorem
(hb : b < 0) : a / b < 1 ↔ b < a
Full source 
theorem div_lt_one_of_neg (hb : b < 0) : a / b < 1 ↔ b < a := by rw [div_lt_iff_of_neg hb, one_mul]
Division by Negative Element Less Than One: $\frac{a}{b} < 1 \leftrightarrow b < a$ when $b < 0$
Informal description
For any element $b < 0$ in a linear ordered field, the inequality $\frac{a}{b} < 1$ holds if and only if $b < a$.
one_div_le_of_neg theorem
(ha : a < 0) (hb : b < 0) : 1 / a ≤ b ↔ 1 / b ≤ a
Full source 
theorem one_div_le_of_neg (ha : a < 0) (hb : b < 0) : 1 / a ≤ b ↔ 1 / b ≤ a := by
  simpa using inv_le_of_neg ha hb
Reciprocal Inequality for Negative Reals: $\frac{1}{a} \leq b \leftrightarrow \frac{1}{b} \leq a$ when $a, b < 0$
Informal description
For any negative real numbers $a$ and $b$, the inequality $\frac{1}{a} \leq b$ holds if and only if $\frac{1}{b} \leq a$.
one_div_lt_of_neg theorem
(ha : a < 0) (hb : b < 0) : 1 / a < b ↔ 1 / b < a
Full source 
theorem one_div_lt_of_neg (ha : a < 0) (hb : b < 0) : 1 / a < b ↔ 1 / b < a := by
  simpa using inv_lt_of_neg ha hb
Reciprocal Inequality for Negative Reals: $\frac{1}{a} < b \leftrightarrow \frac{1}{b} < a$ when $a, b < 0$
Informal description
For any negative real numbers $a$ and $b$, the inequality $\frac{1}{a} < b$ holds if and only if $\frac{1}{b} < a$.
le_one_div_of_neg theorem
(ha : a < 0) (hb : b < 0) : a ≤ 1 / b ↔ b ≤ 1 / a
Full source 
theorem le_one_div_of_neg (ha : a < 0) (hb : b < 0) : a ≤ 1 / b ↔ b ≤ 1 / a := by
  simpa using le_inv_of_neg ha hb
Inequality Between Negative Reals and Their Reciprocals: $a \leq \frac{1}{b} \leftrightarrow b \leq \frac{1}{a}$ when $a, b < 0$
Informal description
For any negative real numbers $a$ and $b$, the inequality $a \leq \frac{1}{b}$ holds if and only if $b \leq \frac{1}{a}$.
lt_one_div_of_neg theorem
(ha : a < 0) (hb : b < 0) : a < 1 / b ↔ b < 1 / a
Full source 
theorem lt_one_div_of_neg (ha : a < 0) (hb : b < 0) : a < 1 / b ↔ b < 1 / a := by
  simpa using lt_inv_of_neg ha hb
Reciprocal Inequality for Negative Reals: $a < \frac{1}{b} \leftrightarrow b < \frac{1}{a}$
Informal description
For any negative real numbers $a$ and $b$, the inequality $a < \frac{1}{b}$ holds if and only if $b < \frac{1}{a}$.
one_lt_div_iff theorem
: 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
Full source 
theorem one_lt_div_iff : 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b := by
  rcases lt_trichotomy b 0 with (hb | rfl | hb)
  · simp [hb, hb.not_lt, one_lt_div_of_neg]
  · simp [lt_irrefl, zero_le_one]
  · simp [hb, hb.not_lt, one_lt_div]
Characterization of $1 < \frac{a}{b}$ in a linearly ordered field
Informal description
For any elements $a$ and $b$ in a linearly ordered field, the inequality $1 < \frac{a}{b}$ holds if and only if either ($0 < b$ and $b < a$) or ($b < 0$ and $a < b$).
one_le_div_iff theorem
: 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
Full source 
theorem one_le_div_iff : 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b := by
  rcases lt_trichotomy b 0 with (hb | rfl | hb)
  · simp [hb, hb.not_lt, one_le_div_of_neg]
  · simp [lt_irrefl, zero_lt_one.not_le, zero_lt_one]
  · simp [hb, hb.not_lt, one_le_div]
Characterization of $1 \leq \frac{a}{b}$ in Ordered Fields
Informal description
For any elements $a$ and $b$ in a linearly ordered field, the inequality $1 \leq \frac{a}{b}$ holds if and only if either: 1. $0 < b$ and $b \leq a$, or 2. $b < 0$ and $a \leq b$.
div_lt_one_iff theorem
: a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
Full source 
theorem div_lt_one_iff : a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a := by
  rcases lt_trichotomy b 0 with (hb | rfl | hb)
  · simp [hb, hb.not_lt, hb.ne, div_lt_one_of_neg]
  · simp [zero_lt_one]
  · simp [hb, hb.not_lt, div_lt_one, hb.ne.symm]
Characterization of $a/b < 1$ in a linearly ordered field
Informal description
For any elements $a$ and $b$ in a linearly ordered field, the inequality $a / b < 1$ holds if and only if one of the following conditions is satisfied: 1. $0 < b$ and $a < b$, or 2. $b = 0$, or 3. $b < 0$ and $b < a$.
div_le_one_iff theorem
: a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
Full source 
theorem div_le_one_iff : a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a := by
  rcases lt_trichotomy b 0 with (hb | rfl | hb)
  · simp [hb, hb.not_lt, hb.ne, div_le_one_of_neg]
  · simp [zero_le_one]
  · simp [hb, hb.not_lt, div_le_one, hb.ne.symm]
Characterization of $a/b \leq 1$ in a linearly ordered field
Informal description
For any elements $a$ and $b$ in a linearly ordered field, the inequality $a / b \leq 1$ holds if and only if one of the following conditions is satisfied: 1. $b$ is positive and $a \leq b$, or 2. $b$ is zero, or 3. $b$ is negative and $b \leq a$.
one_div_le_one_div_of_neg_of_le theorem
(hb : b < 0) (h : a ≤ b) : 1 / b ≤ 1 / a
Full source 
theorem one_div_le_one_div_of_neg_of_le (hb : b < 0) (h : a ≤ b) : 1 / b ≤ 1 / a := by
  rwa [div_le_iff_of_neg' hb, ← div_eq_mul_one_div, div_le_one_of_neg (h.trans_lt hb)]
Reciprocal Inequality for Negative Elements: $\frac{1}{b} \leq \frac{1}{a}$ when $b < 0$ and $a \leq b$
Informal description
For any elements $a$ and $b$ in a linearly ordered field with $b < 0$, if $a \leq b$, then the reciprocal inequality holds: $\frac{1}{b} \leq \frac{1}{a}$.
one_div_lt_one_div_of_neg_of_lt theorem
(hb : b < 0) (h : a < b) : 1 / b < 1 / a
Full source 
theorem one_div_lt_one_div_of_neg_of_lt (hb : b < 0) (h : a < b) : 1 / b < 1 / a := by
  rwa [div_lt_iff_of_neg' hb, ← div_eq_mul_one_div, div_lt_one_of_neg (h.trans hb)]
Reciprocal Inequality for Negative Elements: $\frac{1}{b} < \frac{1}{a}$ when $b < 0$ and $a < b$
Informal description
For any elements $a$ and $b$ in a linearly ordered field with $b < 0$, if $a < b$, then the reciprocal inequality holds: $\frac{1}{b} < \frac{1}{a}$.
le_of_neg_of_one_div_le_one_div theorem
(hb : b < 0) (h : 1 / a ≤ 1 / b) : b ≤ a
Full source 
theorem le_of_neg_of_one_div_le_one_div (hb : b < 0) (h : 1 / a ≤ 1 / b) : b ≤ a :=
  le_imp_le_of_lt_imp_lt (one_div_lt_one_div_of_neg_of_lt hb) h
Order Reversal for Reciprocals of Negative Elements: $\frac{1}{a} \leq \frac{1}{b}$ implies $b \leq a$ when $b < 0$
Informal description
For any elements $a$ and $b$ in a linearly ordered field with $b < 0$, if the inequality $\frac{1}{a} \leq \frac{1}{b}$ holds, then $b \leq a$.
lt_of_neg_of_one_div_lt_one_div theorem
(hb : b < 0) (h : 1 / a < 1 / b) : b < a
Full source 
theorem lt_of_neg_of_one_div_lt_one_div (hb : b < 0) (h : 1 / a < 1 / b) : b < a :=
  lt_imp_lt_of_le_imp_le (one_div_le_one_div_of_neg_of_le hb) h
Order Reversal for Reciprocals of Negative Elements: $\frac{1}{a} < \frac{1}{b}$ implies $b < a$ when $b < 0$
Informal description
For any elements $a$ and $b$ in a linearly ordered field with $b < 0$, if the inequality $\frac{1}{a} < \frac{1}{b}$ holds, then $b < a$.
one_div_le_one_div_of_neg theorem
(ha : a < 0) (hb : b < 0) : 1 / a ≤ 1 / b ↔ b ≤ a
Full source 
/-- 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` -/
theorem one_div_le_one_div_of_neg (ha : a < 0) (hb : b < 0) : 1 / a ≤ 1 / b ↔ b ≤ a := by
  simpa [one_div] using inv_le_inv_of_neg ha hb
Reciprocal Inequality for Negative Reals: $\frac{1}{a} \leq \frac{1}{b} \leftrightarrow b \leq a$ when $a, b < 0$
Informal description
For any negative real numbers $a$ and $b$, the inequality $\frac{1}{a} \leq \frac{1}{b}$ holds if and only if $b \leq a$.
one_div_lt_one_div_of_neg theorem
(ha : a < 0) (hb : b < 0) : 1 / a < 1 / b ↔ b < a
Full source 
/-- For the single implications with fewer assumptions, see `one_div_lt_one_div_of_lt` and
  `lt_of_one_div_lt_one_div` -/
theorem one_div_lt_one_div_of_neg (ha : a < 0) (hb : b < 0) : 1 / a < 1 / b ↔ b < a :=
  lt_iff_lt_of_le_iff_le (one_div_le_one_div_of_neg hb ha)
Reciprocal Inequality for Negative Reals: $\frac{1}{a} < \frac{1}{b} \leftrightarrow b < a$ when $a, b < 0$
Informal description
For any negative real numbers $a$ and $b$, the inequality $\frac{1}{a} < \frac{1}{b}$ holds if and only if $b < a$.
one_div_lt_neg_one theorem
(h1 : a < 0) (h2 : -1 < a) : 1 / a < -1
Full source 
theorem one_div_lt_neg_one (h1 : a < 0) (h2 : -1 < a) : 1 / a < -1 :=
  suffices 1 / a < 1 / -1 by rwa [one_div_neg_one_eq_neg_one] at this
  one_div_lt_one_div_of_neg_of_lt h1 h2
Reciprocal Inequality for Negative Elements Near $-1$: $\frac{1}{a} < -1$ when $-1 < a < 0$
Informal description
For any element $a$ in a linearly ordered field with $a < 0$ and $-1 < a$, the reciprocal of $a$ is less than $-1$, i.e., $\frac{1}{a} < -1$.
one_div_le_neg_one theorem
(h1 : a < 0) (h2 : -1 ≤ a) : 1 / a ≤ -1
Full source 
theorem one_div_le_neg_one (h1 : a < 0) (h2 : -1 ≤ a) : 1 / a ≤ -1 :=
  suffices 1 / a ≤ 1 / -1 by rwa [one_div_neg_one_eq_neg_one] at this
  one_div_le_one_div_of_neg_of_le h1 h2
Reciprocal Inequality for Negative Elements Near $-1$: $\frac{1}{a} \leq -1$ when $-1 \leq a < 0$
Informal description
For any element $a$ in a linearly ordered field with $a < 0$ and $-1 \leq a$, the reciprocal of $a$ satisfies $\frac{1}{a} \leq -1$.
sub_self_div_two theorem
(a : α) : a - a / 2 = a / 2
Full source 
theorem sub_self_div_two (a : α) : a - a / 2 = a / 2 := by
  suffices a / 2 + a / 2 - a / 2 = a / 2 by rwa [add_halves] at this
  rw [add_sub_cancel_right]
Difference Identity: $a - \frac{a}{2} = \frac{a}{2}$
Informal description
For any element $a$ in a linearly ordered field $\alpha$, the difference between $a$ and half of $a$ is equal to half of $a$, i.e., $a - \frac{a}{2} = \frac{a}{2}$.
div_two_sub_self theorem
(a : α) : a / 2 - a = -(a / 2)
Full source 
theorem div_two_sub_self (a : α) : a / 2 - a = -(a / 2) := by
  suffices a / 2 - (a / 2 + a / 2) = -(a / 2) by rwa [add_halves] at this
  rw [sub_add_eq_sub_sub, sub_self, zero_sub]
Difference of Half and Whole Equals Negative Half: $\frac{a}{2} - a = -\frac{a}{2}$
Informal description
For any element $a$ in a linearly ordered field $\alpha$, the difference between half of $a$ and $a$ itself is equal to the negation of half of $a$, i.e., $\frac{a}{2} - a = -\left(\frac{a}{2}\right)$.
add_sub_div_two_lt theorem
(h : a < b) : a + (b - a) / 2 < b
Full source 
theorem add_sub_div_two_lt (h : a < b) : a + (b - a) / 2 < b := by
  rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
    lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two,
    div_lt_div_iff_of_pos_right (zero_lt_two' α)]
Midpoint Inequality: $a + \frac{b - a}{2} < b$ when $a < b$
Informal description
For any elements $a$ and $b$ in a linearly ordered field, if $a < b$, then the midpoint $a + \frac{b - a}{2}$ is strictly less than $b$.
sub_one_div_inv_le_two theorem
(a2 : 2 ≤ a) : (1 - 1 / a)⁻¹ ≤ 2
Full source 
/-- An inequality involving `2`. -/
theorem sub_one_div_inv_le_two (a2 : 2 ≤ a) : (1 - 1 / a)⁻¹ ≤ 2 := by
  -- Take inverses on both sides to obtain `2⁻¹ ≤ 1 - 1 / a`
  refine (inv_anti₀ (inv_pos.2 <| zero_lt_two' α) ?_).trans_eq (inv_inv (2 : α))
  -- move `1 / a` to the left and `2⁻¹` to the right.
  rw [le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le]
  -- take inverses on both sides and use the assumption `2 ≤ a`.
  convert (one_div a).le.trans (inv_anti₀ zero_lt_two a2) using 1
  -- show `1 - 1 / 2 = 1 / 2`.
  rw [sub_eq_iff_eq_add, ← two_mul, mul_inv_cancel₀ two_ne_zero]
Inverse of One Minus Reciprocal Inequality: $(1 - \frac{1}{a})^{-1} \leq 2$ for $a \geq 2$
Informal description
For any element $a$ in a linearly ordered field such that $2 \leq a$, the inequality $(1 - \frac{1}{a})^{-1} \leq 2$ holds.
IsLUB.mul_left theorem
{s : Set α} (ha : 0 ≤ a) (hs : IsLUB s b) : IsLUB ((fun b => a * b) '' s) (a * b)
Full source 
theorem IsLUB.mul_left {s : Set α} (ha : 0 ≤ a) (hs : IsLUB s b) :
    IsLUB ((fun b => a * b) '' s) (a * b) := by
  rcases lt_or_eq_of_le ha with (ha | rfl)
  · exact (OrderIso.mulLeft₀ _ ha).isLUB_image'.2 hs
  · simp_rw [zero_mul]
    rw [hs.nonempty.image_const]
    exact isLUB_singleton
Least upper bound preservation under left multiplication: $\text{sup}(a \cdot s) = a \cdot \text{sup}(s)$ for $a \geq 0$
Informal description
Let $\alpha$ be a linearly ordered field, $s$ a subset of $\alpha$, and $a, b \in \alpha$ with $0 \leq a$. If $b$ is the least upper bound of $s$, then $a \cdot b$ is the least upper bound of the image of $s$ under left multiplication by $a$, i.e., $\{a \cdot x \mid x \in s\}$.
IsLUB.mul_right theorem
{s : Set α} (ha : 0 ≤ a) (hs : IsLUB s b) : IsLUB ((fun b => b * a) '' s) (b * a)
Full source 
theorem IsLUB.mul_right {s : Set α} (ha : 0 ≤ a) (hs : IsLUB s b) :
    IsLUB ((fun b => b * a) '' s) (b * a) := by simpa [mul_comm] using hs.mul_left ha
Least upper bound preservation under right multiplication: $\text{sup}(s \cdot a) = \text{sup}(s) \cdot a$ for $a \geq 0$
Informal description
Let $\alpha$ be a linearly ordered field, $s$ a subset of $\alpha$, and $a, b \in \alpha$ with $0 \leq a$. If $b$ is the least upper bound of $s$, then $b \cdot a$ is the least upper bound of the image of $s$ under right multiplication by $a$, i.e., $\{x \cdot a \mid x \in s\}$.
mul_sub_mul_div_mul_neg_iff theorem
(hc : c ≠ 0) (hd : d ≠ 0) : (a * d - b * c) / (c * d) < 0 ↔ a / c < b / d
Full source 
theorem mul_sub_mul_div_mul_neg_iff (hc : c ≠ 0) (hd : d ≠ 0) :
    (a * d - b * c) / (c * d) < 0 ↔ a / c < b / d := by
  rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_lt_zero]
Negative Cross-Multiplication Inequality: $\frac{ad - bc}{cd} < 0 \leftrightarrow \frac{a}{c} < \frac{b}{d}$
Informal description
For any elements $a, b, c, d$ in a linearly ordered field with $c \neq 0$ and $d \neq 0$, the inequality $\frac{a \cdot d - b \cdot c}{c \cdot d} < 0$ holds if and only if $\frac{a}{c} < \frac{b}{d}$.
mul_sub_mul_div_mul_nonpos_iff theorem
(hc : c ≠ 0) (hd : d ≠ 0) : (a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d
Full source 
theorem mul_sub_mul_div_mul_nonpos_iff (hc : c ≠ 0) (hd : d ≠ 0) :
    (a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d := by
  rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_nonpos]
Inequality of Cross-Multiplication Fractions: $\frac{ad - bc}{cd} \leq 0 \leftrightarrow \frac{a}{c} \leq \frac{b}{d}$
Informal description
For any elements $a, b, c, d$ in a linearly ordered field with $c \neq 0$ and $d \neq 0$, the inequality $\frac{a \cdot d - b \cdot c}{c \cdot d} \leq 0$ holds if and only if $\frac{a}{c} \leq \frac{b}{d}$.
exists_add_lt_and_pos_of_lt theorem
(h : b < a) : ∃ c, b + c < a ∧ 0 < c
Full source 
theorem exists_add_lt_and_pos_of_lt (h : b < a) : ∃ c, b + c < a ∧ 0 < c :=
  ⟨(a - b) / 2, add_sub_div_two_lt h, div_pos (sub_pos_of_lt h) zero_lt_two⟩
Existence of Positive Shift Making Sum Less Than Larger Element: $b < a \implies \exists c > 0, b + c < a$
Informal description
For any elements $a$ and $b$ in a linearly ordered field, if $b < a$, then there exists a positive element $c > 0$ such that $b + c < a$.
le_of_forall_sub_le theorem
(h : ∀ ε > 0, b - ε ≤ a) : b ≤ a
Full source 
theorem le_of_forall_sub_le (h : ∀ ε > 0, b - ε ≤ a) : b ≤ a := by
  contrapose! h
  simpa only [@and_comm ((0 : α) < _), lt_sub_iff_add_lt, gt_iff_lt] using
    exists_add_lt_and_pos_of_lt h
Upper Bound by Arbitrarily Small Shifts: $(\forall \varepsilon > 0, b - \varepsilon \leq a) \implies b \leq a$
Informal description
For any elements $a$ and $b$ in a linearly ordered field, if for every positive $\varepsilon > 0$ we have $b - \varepsilon \leq a$, then $b \leq a$.
le_mul_of_forall_lt₀ theorem
{a b c : α} (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b
Full source 
lemma le_mul_of_forall_lt₀ {a b c : α} (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b := by
  refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_
  obtain ⟨a', ha', hd⟩ := exists_mul_left_lt₀ hd
  obtain ⟨b', hb', hd⟩ := exists_mul_right_lt₀ hd
  exact (h a' ha' b' hb').trans hd.le
Lower Bound on Product via Neighborhood Conditions in Ordered Semifields
Informal description
Let $\alpha$ be a linearly ordered semifield. For any elements $a, b, c \in \alpha$, if for all $a' > a$ and $b' > b$ we have $c \leq a' \cdot b'$, then $c \leq a \cdot b$.
mul_le_of_forall_lt_of_nonneg theorem
{a b c : α} (ha : 0 ≤ a) (hc : 0 ≤ c) (h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c) : a * b ≤ c
Full source 
lemma mul_le_of_forall_lt_of_nonneg {a b c : α} (ha : 0 ≤ a) (hc : 0 ≤ c)
    (h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c) : a * b ≤ c := by
  refine le_of_forall_lt_imp_le_of_dense fun d d_ab ↦ ?_
  rcases lt_or_le d 0 with hd | hd
  · exact hd.le.trans hc
  obtain ⟨a', ha', d_ab⟩ := exists_lt_mul_left_of_nonneg ha hd d_ab
  obtain ⟨b', hb', d_ab⟩ := exists_lt_mul_right_of_nonneg ha'.1 hd d_ab
  exact d_ab.le.trans (h a' ha'.1 ha'.2 b' hb'.1 hb'.2)
Upper bound on product via pointwise bounds: $a \cdot b \leq c$ under nonnegativity and local conditions
Informal description
Let $a, b, c$ be elements of a linearly ordered semifield $\alpha$ such that $a \geq 0$ and $c \geq 0$. If for all $a' \geq 0$ with $a' < a$ and all $b' \geq 0$ with $b' < b$ we have $a' \cdot b' \leq c$, then $a \cdot b \leq c$.
mul_self_inj_of_nonneg theorem
(a0 : 0 ≤ a) (b0 : 0 ≤ b) : a * a = b * b ↔ a = b
Full source 
theorem mul_self_inj_of_nonneg (a0 : 0 ≤ a) (b0 : 0 ≤ b) : a * a = b * b ↔ a = b :=
  mul_self_eq_mul_self_iff.trans <|
    or_iff_left_of_imp fun h => by
      subst a
      have : b = 0 := le_antisymm (neg_nonneg.1 a0) b0
      rw [this, neg_zero]
Square Equality for Nonnegative Reals: $a^2 = b^2 \leftrightarrow a = b$
Informal description
For any nonnegative real numbers $a$ and $b$ (i.e., $a \geq 0$ and $b \geq 0$), the equality $a^2 = b^2$ holds if and only if $a = b$.
min_div_div_right_of_nonpos theorem
(hc : c ≤ 0) (a b : α) : min (a / c) (b / c) = max a b / c
Full source 
theorem min_div_div_right_of_nonpos (hc : c ≤ 0) (a b : α) : min (a / c) (b / c) = max a b / c :=
  Eq.symm <| Antitone.map_max fun _ _ => div_le_div_of_nonpos_of_le hc
Minimum of Divisions by Nonpositive Denominator Equals Maximum Divided by Denominator: $\min(a/c, b/c) = \max(a, b)/c$ for $c \leq 0$
Informal description
For any elements $a, b, c$ in a linearly ordered field with $c \leq 0$, the minimum of $a/c$ and $b/c$ is equal to the maximum of $a$ and $b$ divided by $c$, i.e., $\min(a/c, b/c) = \max(a, b)/c$.
max_div_div_right_of_nonpos theorem
(hc : c ≤ 0) (a b : α) : max (a / c) (b / c) = min a b / c
Full source 
theorem max_div_div_right_of_nonpos (hc : c ≤ 0) (a b : α) : max (a / c) (b / c) = min a b / c :=
  Eq.symm <| Antitone.map_min fun _ _ => div_le_div_of_nonpos_of_le hc
Maximum of Divisions by Nonpositive Denominator Equals Division of Minimum
Informal description
For any elements $a, b, c$ in a linearly ordered field with $c \leq 0$, the maximum of the divisions $a/c$ and $b/c$ is equal to the division of the minimum of $a$ and $b$ by $c$, i.e., \[ \max\left(\frac{a}{c}, \frac{b}{c}\right) = \frac{\min(a, b)}{c}. \]
abs_inv theorem
(a : α) : |a⁻¹| = |a|⁻¹
Full source 
theorem abs_inv (a : α) : |a⁻¹| = |a||a|⁻¹ :=
  map_inv₀ (absHom : α →*₀ α) a
Absolute Value of Inverse Equals Inverse of Absolute Value
Informal description
For any element $a$ in a linear ordered field $\alpha$, the absolute value of the inverse of $a$ is equal to the inverse of the absolute value of $a$, i.e., $|a^{-1}| = |a|^{-1}$.
abs_div theorem
(a b : α) : |a / b| = |a| / |b|
Full source 
theorem abs_div (a b : α) : |a / b| = |a| / |b| :=
  map_div₀ (absHom : α →*₀ α) a b
Absolute Value of Quotient Equals Quotient of Absolute Values
Informal description
For any elements $a$ and $b$ in a linearly ordered field $\alpha$, the absolute value of the quotient $a / b$ is equal to the quotient of the absolute values $|a| / |b|$, i.e., $|a / b| = |a| / |b|$.
abs_one_div theorem
(a : α) : |1 / a| = 1 / |a|
Full source 
theorem abs_one_div (a : α) : |1 / a| = 1 / |a| := by rw [abs_div, abs_one]
Absolute Value of Reciprocal Equals Reciprocal of Absolute Value
Informal description
For any element $a$ in a linearly ordered field $\alpha$, the absolute value of the reciprocal $1/a$ is equal to the reciprocal of the absolute value of $a$, i.e., $|1/a| = 1/|a|$.
uniform_continuous_npow_on_bounded theorem
(B : α) {ε : α} (hε : 0 < ε) (n : ℕ) : ∃ δ > 0, ∀ q r : α, |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
Full source 
theorem uniform_continuous_npow_on_bounded (B : α) {ε : α} (hε : 0 < ε) (n : ℕ) :
    ∃ δ > 0, ∀ q r : α, |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε := by
  wlog B_pos : 0 < B generalizing B
  · have ⟨δ, δ_pos, cont⟩ := this 1 zero_lt_one
    exact ⟨δ, δ_pos, fun q r hr ↦ cont q r (hr.trans ((le_of_not_lt B_pos).trans zero_le_one))⟩
  have pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1) := zero_lt_one.trans_le <| le_add_of_nonneg_right <|
    mul_nonneg n.cast_nonneg <| (pow_pos (B_pos.trans <| lt_add_of_pos_right _ zero_lt_one) _).le
  refine ⟨min 1 (ε / (1 + n * (B + 1) ^ (n - 1))), lt_min zero_lt_one (div_pos hε pos),
    fun q r hr hqr ↦ (abs_pow_sub_pow_le ..).trans_lt ?_⟩
  rw [le_inf_iff, le_div_iff₀ pos, mul_one_add, ← mul_assoc] at hqr
  obtain h | h := (abs_nonneg (q - r)).eq_or_lt
  · simpa only [← h, zero_mul] using hε
  refine (lt_of_le_of_lt ?_ <| lt_add_of_pos_left _ h).trans_le hqr.2
  refine mul_le_mul_of_nonneg_left (pow_le_pow_left₀ ((abs_nonneg _).trans le_sup_left) ?_ _)
    (mul_nonneg (abs_nonneg _) n.cast_nonneg)
  refine max_le ?_ (hr.trans <| le_add_of_nonneg_right zero_le_one)
  exact add_sub_cancel r q ▸ (abs_add_le ..).trans (add_le_add hr hqr.1)
Uniform Continuity of Power Function on Bounded Sets: $|q^n - r^n| < \varepsilon$ for $|r| \leq B$ and $|q - r| \leq \delta$
Informal description
For any element $B$ in a linearly ordered field $\alpha$, any positive $\varepsilon > 0$, and any natural number $n$, there exists a $\delta > 0$ such that for all $q, r \in \alpha$ with $|r| \leq B$ and $|q - r| \leq \delta$, the inequality $|q^n - r^n| < \varepsilon$ holds.
Mathlib.Meta.Positivity.evalDiv definition
: PositivityExt
Full source 
/-- The `positivity` extension which identifies expressions of the form `a / b`,
such that `positivity` successfully recognises both `a` and `b`. -/
@[positivity _ / _] def evalDiv : PositivityExt where eval {u α} zα pα e := do
  let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e)
    | throwError "not /"
  let _e_eq : $e =Q $f $a $b := ⟨⟩
  let _a ← synthInstanceQ q(Semifield $α)
  let _a ← synthInstanceQ q(LinearOrder $α)
  let _a ← synthInstanceQ q(IsStrictOrderedRing $α)
  assumeInstancesCommute
  let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(HDiv.hDiv)
  let ra ← core zα pα a; let rb ← core zα pα b
  match ra, rb with
  | .positive pa, .positive pb => pure (.positive q(div_pos $pa $pb))
  | .positive pa, .nonnegative pb => pure (.nonnegative q(div_nonneg_of_pos_of_nonneg $pa $pb))
  | .nonnegative pa, .positive pb => pure (.nonnegative q(div_nonneg_of_nonneg_of_pos $pa $pb))
  | .nonnegative pa, .nonnegative pb => pure (.nonnegative q(div_nonneg $pa $pb))
  | .positive pa, .nonzero pb => pure (.nonzero q(div_ne_zero_of_pos_of_ne_zero $pa $pb))
  | .nonzero pa, .positive pb => pure (.nonzero q(div_ne_zero_of_ne_zero_of_pos $pa $pb))
  | .nonzero pa, .nonzero pb => pure (.nonzero q(div_ne_zero $pa $pb))
  | _, _ => pure .none
Positivity of division in linear ordered semifields
Informal description
The `positivity` extension which identifies expressions of the form \( a / b \) in a linear ordered semifield \( \alpha \), where the `positivity` tactic successfully recognizes both \( a \) and \( b \). The extension returns the appropriate positivity property (positive, non-negative, or non-zero) of the division expression based on the properties of \( a \) and \( b \). Specifically, the extension handles the following cases: - If both \( a \) and \( b \) are positive, then \( a / b \) is positive. - If \( a \) is positive and \( b \) is non-negative, then \( a / b \) is non-negative. - If \( a \) is non-negative and \( b \) is positive, then \( a / b \) is non-negative. - If both \( a \) and \( b \) are non-negative, then \( a / b \) is non-negative. - If \( a \) is positive and \( b \) is non-zero, then \( a / b \) is non-zero. - If \( a \) is non-zero and \( b \) is positive, then \( a / b \) is non-zero. - If both \( a \) and \( b \) are non-zero, then \( a / b \) is non-zero.
Mathlib.Meta.Positivity.evalInv definition
: PositivityExt
Full source 
/-- The `positivity` extension which identifies expressions of the form `a⁻¹`,
such that `positivity` successfully recognises `a`. -/
@[positivity _⁻¹]
def evalInv : PositivityExt where eval {u α} zα pα e := do
  let .app (f : Q($α → $α)) (a : Q($α)) ← withReducible (whnf e) | throwError "not ⁻¹"
  let _e_eq : $e =Q $f $a := ⟨⟩
  let _a ← synthInstanceQ q(Semifield $α)
  let _a ← synthInstanceQ q(LinearOrder $α)
  let _a ← synthInstanceQ q(IsStrictOrderedRing $α)
  assumeInstancesCommute
  let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(Inv.inv)
  let ra ← core zα pα a
  match ra with
  | .positive pa => pure (.positive q(inv_pos_of_pos $pa))
  | .nonnegative pa => pure (.nonnegative q(inv_nonneg_of_nonneg $pa))
  | .nonzero pa => pure (.nonzero q(inv_ne_zero $pa))
  | .none => pure .none
Positivity analysis for inverses
Informal description
The `positivity` extension which identifies expressions of the form \( a^{-1} \) and determines their positivity properties based on the positivity of \( a \). Specifically: - If \( a \) is positive, then \( a^{-1} \) is positive. - If \( a \) is non-negative, then \( a^{-1} \) is non-negative. - If \( a \) is non-zero, then \( a^{-1} \) is non-zero.
Mathlib.Meta.Positivity.evalPowZeroInt definition
: PositivityExt
Full source 
/-- The `positivity` extension which identifies expressions of the form `a ^ (0:ℤ)`. -/
@[positivity _ ^ (0 : ℤ), Pow.pow _ (0 : ℤ)]
def evalPowZeroInt : PositivityExt where eval {u α} _zα _pα e := do
  let .app (.app _ (a : Q($α))) _ ← withReducible (whnf e) | throwError "not ^"
  let _a ← synthInstanceQ q(Semifield $α)
  let _a ← synthInstanceQ q(LinearOrder $α)
  let _a ← synthInstanceQ q(IsStrictOrderedRing $α)
  assumeInstancesCommute
  let ⟨_a⟩ ← Qq.assertDefEqQ q($e) q($a ^ (0 : ℤ))
  pure (.positive q(zpow_zero_pos $a))
Positivity of integer power zero
Informal description
The `positivity` extension which identifies expressions of the form \( a^0 \) (where \( 0 \) is an integer) as positive in a linear ordered semifield \( \alpha \).