Documentation

Mathlib.Algebra.Order.Field.Basic

Lemmas about linear ordered (semi)fields #

@[simp]
theorem OrderIso.mulLeft₀_apply {α : Type u_2} [LinearOrderedSemifield α] (a : α) (ha : 0 < a) (x : α) :
(OrderIso.mulLeft₀ a ha) x = a * x
@[simp]
theorem OrderIso.mulLeft₀_symm_apply {α : Type u_2} [LinearOrderedSemifield α] (a : α) (ha : 0 < a) (x : α) :
def OrderIso.mulLeft₀ {α : Type u_2} [LinearOrderedSemifield α] (a : α) (ha : 0 < a) :
α ≃o α

Equiv.mulLeft₀ as an order_iso.

Equations
Instances For
    @[simp]
    theorem OrderIso.mulRight₀_apply {α : Type u_2} [LinearOrderedSemifield α] (a : α) (ha : 0 < a) (x : α) :
    (OrderIso.mulRight₀ a ha) x = x * a
    @[simp]
    theorem OrderIso.mulRight₀_symm_apply {α : Type u_2} [LinearOrderedSemifield α] (a : α) (ha : 0 < a) (x : α) :
    def OrderIso.mulRight₀ {α : Type u_2} [LinearOrderedSemifield α] (a : α) (ha : 0 < a) :
    α ≃o α

    Equiv.mulRight₀ as an order_iso.

    Equations
    Instances For

      Relating one division with another term. #

      theorem le_div_iff {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hc : 0 < c) :
      a b / c a * c b
      theorem le_div_iff' {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hc : 0 < c) :
      a b / c c * a b
      theorem div_le_iff {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hb : 0 < b) :
      a / b c a c * b
      theorem div_le_iff' {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hb : 0 < b) :
      a / b c a b * c
      theorem div_le_comm₀ {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hb : 0 < b) (hc : 0 < c) :
      a / b c a / c b
      theorem lt_div_iff {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hc : 0 < c) :
      a < b / c a * c < b
      theorem lt_div_iff' {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hc : 0 < c) :
      a < b / c c * a < b
      theorem div_lt_iff {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hc : 0 < c) :
      b / c < a b < a * c
      theorem div_lt_iff' {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hc : 0 < c) :
      b / c < a b < c * a
      theorem div_lt_comm₀ {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hb : 0 < b) (hc : 0 < c) :
      a / b < c a / c < b
      theorem inv_mul_le_iff {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : 0 < b) :
      b⁻¹ * a c a b * c
      theorem inv_mul_le_iff' {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : 0 < b) :
      b⁻¹ * a c a c * b
      theorem mul_inv_le_iff {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : 0 < b) :
      a * b⁻¹ c a b * c
      theorem mul_inv_le_iff' {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : 0 < b) :
      a * b⁻¹ c a c * b
      theorem div_self_le_one {α : Type u_2} [LinearOrderedSemifield α] (a : α) :
      a / a 1
      theorem inv_mul_lt_iff {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : 0 < b) :
      b⁻¹ * a < c a < b * c
      theorem inv_mul_lt_iff' {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : 0 < b) :
      b⁻¹ * a < c a < c * b
      theorem mul_inv_lt_iff {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : 0 < b) :
      a * b⁻¹ < c a < b * c
      theorem mul_inv_lt_iff' {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : 0 < b) :
      a * b⁻¹ < c a < c * b
      theorem inv_pos_le_iff_one_le_mul {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) :
      a⁻¹ b 1 b * a
      theorem inv_pos_le_iff_one_le_mul' {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) :
      a⁻¹ b 1 a * b
      theorem inv_pos_lt_iff_one_lt_mul {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) :
      a⁻¹ < b 1 < b * a
      theorem inv_pos_lt_iff_one_lt_mul' {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) :
      a⁻¹ < b 1 < a * b
      theorem div_le_of_nonneg_of_le_mul {α : Type u_2} [LinearOrderedSemifield α] {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)

      theorem mul_le_of_nonneg_of_le_div {α : Type u_2} [LinearOrderedSemifield α] {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)

      theorem div_le_one_of_le {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (h : a b) (hb : 0 b) :
      a / b 1
      theorem mul_inv_le_one_of_le {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (h : a b) (hb : 0 b) :
      a * b⁻¹ 1
      theorem inv_mul_le_one_of_le {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (h : a b) (hb : 0 b) :
      b⁻¹ * a 1

      Bi-implications of inequalities using inversions #

      theorem inv_le_inv_of_le {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) (h : a b) :
      theorem inv_le_inv {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) :

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

      theorem inv_le {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) :

      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.

      theorem inv_le_of_inv_le {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) (h : a⁻¹ b) :
      theorem le_inv {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) :
      theorem inv_lt_inv {α : Type u_2} [LinearOrderedSemifield α] {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.

      theorem inv_lt_inv_of_lt {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (hb : 0 < b) (h : b < a) :
      theorem inv_lt {α : Type u_2} [LinearOrderedSemifield α] {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.

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

      Relating two divisions. #

      theorem div_le_div_of_nonneg_right {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hab : a b) (hc : 0 c) :
      a / c b / c
      theorem div_lt_div_of_pos_right {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : a < b) (hc : 0 < c) :
      a / c < b / c
      theorem div_le_div_of_nonneg_left {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (ha : 0 a) (hc : 0 < c) (h : c b) :
      a / b a / c
      theorem div_lt_div_of_pos_left {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (ha : 0 < a) (hc : 0 < c) (h : c < b) :
      a / b < a / c
      @[deprecated div_le_div_of_nonneg_right]
      theorem div_le_div_of_le_of_nonneg {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hab : a b) (hc : 0 c) :
      a / c b / c

      Alias of div_le_div_of_nonneg_right.

      @[deprecated div_lt_div_of_pos_right]
      theorem div_lt_div_of_lt {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (h : a < b) (hc : 0 < c) :
      a / c < b / c

      Alias of div_lt_div_of_pos_right.

      @[deprecated div_le_div_of_nonneg_left]
      theorem div_le_div_of_le_left {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (ha : 0 a) (hc : 0 < c) (h : c b) :
      a / b a / c

      Alias of div_le_div_of_nonneg_left.

      @[deprecated div_lt_div_of_pos_left]
      theorem div_lt_div_of_lt_left {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (ha : 0 < a) (hc : 0 < c) (h : c < b) :
      a / b < a / c

      Alias of div_lt_div_of_pos_left.

      @[deprecated div_le_div_of_nonneg_right]
      theorem div_le_div_of_le {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hc : 0 c) (hab : a b) :
      a / c b / c
      theorem div_le_div_right {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hc : 0 < c) :
      a / c b / c a b
      theorem div_lt_div_right {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (hc : 0 < c) :
      a / c < b / c a < b
      theorem div_lt_div_left {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
      a / b < a / c c < b
      theorem div_le_div_left {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
      a / b a / c c b
      theorem div_lt_div_iff {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} {d : α} (b0 : 0 < b) (d0 : 0 < d) :
      a / b < c / d a * d < c * b
      theorem div_le_div_iff {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} {d : α} (b0 : 0 < b) (d0 : 0 < d) :
      a / b c / d a * d c * b
      theorem div_le_div {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} {d : α} (hc : 0 c) (hac : a c) (hd : 0 < d) (hbd : d b) :
      a / b c / d
      theorem div_lt_div {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} {d : α} (hac : a < c) (hbd : d b) (c0 : 0 c) (d0 : 0 < d) :
      a / b < c / d
      theorem div_lt_div' {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} {d : α} (hac : a c) (hbd : d < b) (c0 : 0 < c) (d0 : 0 < d) :
      a / b < c / d

      Relating one division and involving 1 #

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

      Relating two divisions, involving 1 #

      theorem one_div_le_one_div_of_le {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) (h : a b) :
      1 / b 1 / a
      theorem one_div_lt_one_div_of_lt {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) (h : a < b) :
      1 / b < 1 / a
      theorem le_of_one_div_le_one_div {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) (h : 1 / a 1 / b) :
      b a
      theorem lt_of_one_div_lt_one_div {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) (h : 1 / a < 1 / b) :
      b < a
      theorem one_div_le_one_div {α : Type u_2} [LinearOrderedSemifield α] {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

      theorem one_div_lt_one_div {α : Type u_2} [LinearOrderedSemifield α] {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

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

      Results about halving. #

      The equalities also hold in semifields of characteristic 0.

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

      Alias of the reverse direction of half_le_self_iff.

      theorem half_lt_self {α : Type u_2} [LinearOrderedSemifield α] {a : α} :
      0 < aa / 2 < a

      Alias of the reverse direction of half_lt_self_iff.

      theorem div_two_lt_of_pos {α : Type u_2} [LinearOrderedSemifield α] {a : α} :
      0 < aa / 2 < a

      Alias of the reverse direction of half_lt_self_iff.


      Alias of the reverse direction of half_lt_self_iff.

      theorem one_half_lt_one {α : Type u_2} [LinearOrderedSemifield α] :
      1 / 2 < 1
      theorem left_lt_add_div_two {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} :
      a < (a + b) / 2 a < b
      theorem add_div_two_lt_right {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} :
      (a + b) / 2 < b a < b
      theorem add_thirds {α : Type u_2} [LinearOrderedSemifield α] (a : α) :
      a / 3 + a / 3 + a / 3 = a

      Miscellaneous lemmas #

      @[simp]
      theorem div_pos_iff_of_pos_left {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) :
      0 < a / b 0 < b
      @[simp]
      theorem div_pos_iff_of_pos_right {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} (hb : 0 < b) :
      0 < a / b 0 < a
      theorem mul_le_mul_of_mul_div_le {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} {d : α} (h : a * (b / c) d) (hc : 0 < c) :
      b * a d * c
      theorem div_mul_le_div_mul_of_div_le_div {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {c : α} {d : α} {e : α} (h : a / b c / d) (he : 0 e) :
      a / (b * e) c / (d * e)
      theorem exists_pos_mul_lt {α : Type u_2} [LinearOrderedSemifield α] {a : α} (h : 0 < a) (b : α) :
      ∃ (c : α), 0 < c b * c < a
      theorem exists_pos_lt_mul {α : Type u_2} [LinearOrderedSemifield α] {a : α} (h : 0 < a) (b : α) :
      ∃ (c : α), 0 < c b < c * a
      theorem monotone_div_right_of_nonneg {α : Type u_2} [LinearOrderedSemifield α] {a : α} (ha : 0 a) :
      Monotone fun (x : α) => x / a
      theorem strictMono_div_right_of_pos {α : Type u_2} [LinearOrderedSemifield α] {a : α} (ha : 0 < a) :
      StrictMono fun (x : α) => x / a
      theorem Monotone.div_const {α : Type u_2} [LinearOrderedSemifield α] {β : Type u_4} [Preorder β] {f : βα} (hf : Monotone f) {c : α} (hc : 0 c) :
      Monotone fun (x : β) => f x / c
      theorem StrictMono.div_const {α : Type u_2} [LinearOrderedSemifield α] {β : Type u_4} [Preorder β] {f : βα} (hf : StrictMono f) {c : α} (hc : 0 < c) :
      StrictMono fun (x : β) => f x / c
      @[instance 100]
      Equations
      • =
      theorem min_div_div_right {α : Type u_2} [LinearOrderedSemifield α] {c : α} (hc : 0 c) (a : α) (b : α) :
      min (a / c) (b / c) = min a b / c
      theorem max_div_div_right {α : Type u_2} [LinearOrderedSemifield α] {c : α} (hc : 0 c) (a : α) (b : α) :
      max (a / c) (b / c) = max a b / c
      theorem one_div_strictAntiOn {α : Type u_2} [LinearOrderedSemifield α] :
      StrictAntiOn (fun (x : α) => 1 / x) (Set.Ioi 0)
      theorem one_div_pow_le_one_div_pow_of_le {α : Type u_2} [LinearOrderedSemifield α] {a : α} (a1 : 1 a) {m : } {n : } (mn : m n) :
      1 / a ^ n 1 / a ^ m
      theorem one_div_pow_lt_one_div_pow_of_lt {α : Type u_2} [LinearOrderedSemifield α] {a : α} (a1 : 1 < a) {m : } {n : } (mn : m < n) :
      1 / a ^ n < 1 / a ^ m
      theorem one_div_pow_anti {α : Type u_2} [LinearOrderedSemifield α] {a : α} (a1 : 1 a) :
      Antitone fun (n : ) => 1 / a ^ n
      theorem one_div_pow_strictAnti {α : Type u_2} [LinearOrderedSemifield α] {a : α} (a1 : 1 < a) :
      StrictAnti fun (n : ) => 1 / a ^ n
      theorem inv_strictAntiOn {α : Type u_2} [LinearOrderedSemifield α] :
      StrictAntiOn (fun (x : α) => x⁻¹) (Set.Ioi 0)
      theorem inv_pow_le_inv_pow_of_le {α : Type u_2} [LinearOrderedSemifield α] {a : α} (a1 : 1 a) {m : } {n : } (mn : m n) :
      (a ^ n)⁻¹ (a ^ m)⁻¹
      theorem inv_pow_lt_inv_pow_of_lt {α : Type u_2} [LinearOrderedSemifield α] {a : α} (a1 : 1 < a) {m : } {n : } (mn : m < n) :
      (a ^ n)⁻¹ < (a ^ m)⁻¹
      theorem inv_pow_anti {α : Type u_2} [LinearOrderedSemifield α] {a : α} (a1 : 1 a) :
      Antitone fun (n : ) => (a ^ n)⁻¹
      theorem inv_pow_strictAnti {α : Type u_2} [LinearOrderedSemifield α] {a : α} (a1 : 1 < a) :
      StrictAnti fun (n : ) => (a ^ n)⁻¹

      Results about IsGLB #

      theorem IsGLB.mul_left {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {s : Set α} (ha : 0 a) (hs : IsGLB s b) :
      IsGLB ((fun (b : α) => a * b) '' s) (a * b)
      theorem IsGLB.mul_right {α : Type u_2} [LinearOrderedSemifield α] {a : α} {b : α} {s : Set α} (ha : 0 a) (hs : IsGLB s b) :
      IsGLB ((fun (b : α) => b * a) '' s) (b * a)

      Lemmas about pos, nonneg, nonpos, neg #

      theorem div_pos_iff {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} :
      0 < a / b 0 < a 0 < b a < 0 b < 0
      theorem div_neg_iff {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} :
      a / b < 0 0 < a b < 0 a < 0 0 < b
      theorem div_nonneg_iff {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} :
      0 a / b 0 a 0 b a 0 b 0
      theorem div_nonpos_iff {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} :
      a / b 0 0 a b 0 a 0 0 b
      theorem div_nonneg_of_nonpos {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} (ha : a 0) (hb : b 0) :
      0 a / b
      theorem div_pos_of_neg_of_neg {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} (ha : a < 0) (hb : b < 0) :
      0 < a / b
      theorem div_neg_of_neg_of_pos {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} (ha : a < 0) (hb : 0 < b) :
      a / b < 0
      theorem div_neg_of_pos_of_neg {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} (ha : 0 < a) (hb : b < 0) :
      a / b < 0

      Relating one division with another term #

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

      Bi-implications of inequalities using inversions #

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

      Monotonicity results involving inversion #

      theorem sub_inv_antitoneOn_Ioi {α : Type u_2} [LinearOrderedField α] {c : α} :
      AntitoneOn (fun (x : α) => (x - c)⁻¹) (Set.Ioi c)
      theorem sub_inv_antitoneOn_Iio {α : Type u_2} [LinearOrderedField α] {c : α} :
      AntitoneOn (fun (x : α) => (x - c)⁻¹) (Set.Iio c)
      theorem sub_inv_antitoneOn_Icc_right {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} {c : α} (ha : c < a) :
      AntitoneOn (fun (x : α) => (x - c)⁻¹) (Set.Icc a b)
      theorem sub_inv_antitoneOn_Icc_left {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} {c : α} (ha : b < c) :
      AntitoneOn (fun (x : α) => (x - c)⁻¹) (Set.Icc a b)
      theorem inv_antitoneOn_Ioi {α : Type u_2} [LinearOrderedField α] :
      AntitoneOn (fun (x : α) => x⁻¹) (Set.Ioi 0)
      theorem inv_antitoneOn_Iio {α : Type u_2} [LinearOrderedField α] :
      AntitoneOn (fun (x : α) => x⁻¹) (Set.Iio 0)
      theorem inv_antitoneOn_Icc_right {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} (ha : 0 < a) :
      AntitoneOn (fun (x : α) => x⁻¹) (Set.Icc a b)
      theorem inv_antitoneOn_Icc_left {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} (hb : b < 0) :
      AntitoneOn (fun (x : α) => x⁻¹) (Set.Icc a b)

      Relating two divisions #

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

      Relating one division and involving 1 #

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

      Relating two divisions, involving 1 #

      theorem one_div_le_one_div_of_neg_of_le {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} (hb : b < 0) (h : a b) :
      1 / b 1 / a
      theorem one_div_lt_one_div_of_neg_of_lt {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} (hb : b < 0) (h : a < b) :
      1 / b < 1 / a
      theorem le_of_neg_of_one_div_le_one_div {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} (hb : b < 0) (h : 1 / a 1 / b) :
      b a
      theorem lt_of_neg_of_one_div_lt_one_div {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} (hb : b < 0) (h : 1 / a < 1 / b) :
      b < a
      theorem one_div_le_one_div_of_neg {α : Type u_2} [LinearOrderedField α] {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

      theorem one_div_lt_one_div_of_neg {α : Type u_2} [LinearOrderedField α] {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

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

      Results about halving #

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

      An inequality involving 2.

      Results about IsLUB #

      theorem IsLUB.mul_left {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} {s : Set α} (ha : 0 a) (hs : IsLUB s b) :
      IsLUB ((fun (b : α) => a * b) '' s) (a * b)
      theorem IsLUB.mul_right {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} {s : Set α} (ha : 0 a) (hs : IsLUB s b) :
      IsLUB ((fun (b : α) => b * a) '' s) (b * a)

      Miscellaneous lemmas #

      theorem mul_sub_mul_div_mul_neg_iff {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} {c : α} {d : α} (hc : c 0) (hd : d 0) :
      (a * d - b * c) / (c * d) < 0 a / c < b / d
      theorem mul_sub_mul_div_mul_nonpos_iff {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} {c : α} {d : α} (hc : c 0) (hd : d 0) :
      (a * d - b * c) / (c * d) 0 a / c b / d
      theorem div_lt_div_of_mul_sub_mul_div_neg {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} {c : α} {d : α} (hc : c 0) (hd : d 0) :
      (a * d - b * c) / (c * d) < 0a / c < b / d

      Alias of the forward direction of mul_sub_mul_div_mul_neg_iff.

      theorem mul_sub_mul_div_mul_neg {α : Type u_2} [LinearOrderedField α] {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.

      theorem div_le_div_of_mul_sub_mul_div_nonpos {α : Type u_2} [LinearOrderedField α] {a : α} {b : α} {c : α} {d : α} (hc : c 0) (hd : d 0) :
      (a * d - b * c) / (c * d) 0a / c b / d

      Alias of the forward direction of mul_sub_mul_div_mul_nonpos_iff.

      theorem mul_sub_mul_div_mul_nonpos {α : Type u_2} [LinearOrderedField α] {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.

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

      The positivity extension which identifies expressions of the form a / b, such that positivity successfully recognises both a and b.

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

        The positivity extension which identifies expressions of the form a⁻¹, such that positivity successfully recognises a.

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

          The positivity extension which identifies expressions of the form a ^ (0:ℤ).

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