Lemmas about linear ordered (semi)fields

Relating two divisions.

@[deprecated div_le_div_iff_of_pos_right (since := "2024-11-12")]

theorem div_le_div_right {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : 0 < c) : a / c ≤ b / c ↔ a ≤ b

@[deprecated div_lt_div_iff_of_pos_right (since := "2024-11-12")]

theorem div_lt_div_right {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : 0 < c) : a / c < b / c ↔ a < b

@[deprecated div_lt_div_iff_of_pos_left (since := "2024-11-13")]

theorem div_lt_div_left {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b < a / c ↔ c < b

@[deprecated div_le_div_iff_of_pos_left (since := "2024-11-12")]

theorem div_le_div_left {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b ≤ a / c ↔ c ≤ b

@[deprecated div_lt_div_iff₀ (since := "2024-11-12")]

theorem div_lt_div_iff {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b c d : α} (b0 : 0 < b) (d0 : 0 < d) : a / b < c / d ↔ a * d < c * b

@[deprecated div_le_div_iff₀ (since := "2024-11-12")]

theorem div_le_div_iff {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b c d : α} (b0 : 0 < b) (d0 : 0 < d) : a / b ≤ c / d ↔ a * d ≤ c * b

@[deprecated div_le_div₀ (since := "2024-11-12")]

theorem div_le_div {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b c d : α} (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hbd : d ≤ b) : a / b ≤ c / d

@[deprecated div_lt_div₀ (since := "2024-11-12")]

theorem div_lt_div {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b c d : α} (hac : a < c) (hbd : d ≤ b) (c0 : 0 ≤ c) (d0 : 0 < d) : a / b < c / d

@[deprecated div_lt_div₀' (since := "2024-11-12")]

theorem div_lt_div' {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : 0 ≤ a) (hb : 1 ≤ b) : a / b ≤ a

theorem div_lt_self {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) (hb : 1 < b) : a / b < a

theorem le_div_self {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : 0 ≤ a) (hb₀ : 0 < b) (hb₁ : b ≤ 1) : a ≤ a / b

theorem one_le_div {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a

theorem div_le_one {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (hb : 0 < b) : a / b ≤ 1 ↔ a ≤ b

theorem one_lt_div {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (hb : 0 < b) : 1 < a / b ↔ b < a

theorem div_lt_one {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (hb : 0 < b) : a / b < 1 ↔ a < b

theorem one_div_le {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) (hb : 0 < b) : 1 / a ≤ b ↔ 1 / b ≤ a

theorem one_div_lt {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) (hb : 0 < b) : 1 / a < b ↔ 1 / b < a

theorem le_one_div {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) (hb : 0 < b) : a ≤ 1 / b ↔ b ≤ 1 / a

theorem lt_one_div {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) (hb : 0 < b) : a < 1 / b ↔ b < 1 / a

theorem Bound.one_lt_div_of_pos_of_lt {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (b0 : 0 < b) : b < a → 1 < a / b

theorem Bound.div_lt_one_of_pos_of_lt {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (b0 : 0 < b) : a < b → a / b < 1

Relating two divisions, involving 1

theorem one_div_le_one_div_of_le {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) (h : a ≤ b) : 1 / b ≤ 1 / a

theorem one_div_lt_one_div_of_lt {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) (h : a < b) : 1 / b < 1 / a

theorem le_of_one_div_le_one_div {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) (h : 1 / a ≤ 1 / b) : b ≤ a

theorem lt_of_one_div_lt_one_div {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) (h : 1 / a < 1 / b) : b < a

theorem one_div_le_one_div {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (h1 : 0 < a) (h2 : a < 1) : 1 < 1 / a

theorem one_le_one_div {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (h1 : 0 < a) (h2 : a ≤ 1) : 1 ≤ 1 / a

Results about halving.

The equalities also hold in semifields of characteristic 0.

theorem half_pos {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (h : 0 < a) : 0 < a / 2

theorem one_half_pos {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] : 0 < 1 / 2

@[simp]

theorem half_le_self_iff {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} : a / 2 ≤ a ↔ 0 ≤ a

@[simp]

theorem half_lt_self_iff {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} : a / 2 < a ↔ 0 < a

theorem half_le_self {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} : 0 ≤ a → a / 2 ≤ a

Alias of the reverse direction of half_le_self_iff.

theorem half_lt_self {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} : 0 < a → a / 2 < a

Alias of the reverse direction of half_lt_self_iff.

theorem div_two_lt_of_pos {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} : 0 < a → a / 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} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] : 1 / 2 < 1

theorem two_inv_lt_one {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] : 2⁻¹ < 1

theorem left_lt_add_div_two {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : a < (a + b) / 2 ↔ a < b

theorem add_div_two_lt_right {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : (a + b) / 2 < b ↔ a < b

theorem add_thirds {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) : a / 3 + a / 3 + a / 3 = a

Miscellaneous lemmas

@[simp]

theorem div_pos_iff_of_pos_left {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) : 0 < a / b ↔ 0 < b

@[simp]

theorem div_pos_iff_of_pos_right {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (hb : 0 < b) : 0 < a / b ↔ 0 < a

theorem mul_le_mul_of_mul_div_le {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (h : 0 < a) (b : α) : ∃ (c : α), 0 < c ∧ b * c < a

theorem exists_pos_lt_mul {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (h : 0 < a) (b : α) : ∃ (c : α), 0 < c ∧ b < c * a

theorem monotone_div_right_of_nonneg {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (ha : 0 ≤ a) : Monotone fun (x : α) => x / a

theorem strictMono_div_right_of_pos {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (ha : 0 < a) : StrictMono fun (x : α) => x / a

theorem Monotone.div_const {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {β : 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} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_4} [Preorder β] {f : β → α} (hf : StrictMono f) {c : α} (hc : 0 < c) : StrictMono fun (x : β) => f x / c

@[instance 100]

instance LinearOrderedSemiField.toDenselyOrdered {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] : DenselyOrdered α

theorem min_div_div_right {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} (hc : 0 ≤ c) (a b : α) : a / c ⊓ b / c = (a ⊓ b) / c

theorem max_div_div_right {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} (hc : 0 ≤ c) (a b : α) : a / c ⊔ b / c = (a ⊔ b) / c

theorem one_div_strictAntiOn {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] : StrictAntiOn (fun (x : α) => 1 / x) (Set.Ioi 0)

theorem one_div_pow_le_one_div_pow_of_le {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (a1 : 1 < a) {m n : ℕ} (mn : m < n) : 1 / a ^ n < 1 / a ^ m

theorem one_div_pow_anti {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (a1 : 1 ≤ a) : Antitone fun (n : ℕ) => 1 / a ^ n

theorem one_div_pow_strictAnti {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (a1 : 1 < a) : StrictAnti fun (n : ℕ) => 1 / a ^ n

theorem inv_strictAntiOn {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] : StrictAntiOn (fun (x : α) => x⁻¹) (Set.Ioi 0)

theorem inv_pow_le_inv_pow_of_le {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (a1 : 1 ≤ a) {m n : ℕ} (mn : m ≤ n) : (a ^ n)⁻¹ ≤ (a ^ m)⁻¹

theorem inv_pow_lt_inv_pow_of_lt {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (a1 : 1 < a) {m n : ℕ} (mn : m < n) : (a ^ n)⁻¹ < (a ^ m)⁻¹

theorem inv_pow_anti {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (a1 : 1 ≤ a) : Antitone fun (n : ℕ) => (a ^ n)⁻¹

theorem inv_pow_strictAnti {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (a1 : 1 < a) : StrictAnti fun (n : ℕ) => (a ^ n)⁻¹

theorem le_iff_forall_one_lt_le_mul₀ {α : Type u_4} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (hb : 0 ≤ b) : a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε

Results about IsGLB

theorem IsGLB.mul_left {α : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : 0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

theorem div_neg_iff {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

theorem div_nonneg_iff {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : 0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem div_nonpos_iff {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

theorem div_nonneg_of_nonpos {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a / b

theorem div_pos_of_neg_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : 0 < a / b

theorem div_neg_of_neg_of_pos {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : 0 < b) : a / b < 0

theorem div_neg_of_pos_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : b / c ≤ a ↔ a * c ≤ b

theorem div_le_iff_of_neg' {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : b / c ≤ a ↔ c * a ≤ b

theorem le_div_iff_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : a ≤ b / c ↔ b ≤ a * c

theorem le_div_iff_of_neg' {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : a ≤ b / c ↔ b ≤ c * a

theorem div_lt_iff_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : b / c < a ↔ a * c < b

theorem div_lt_iff_of_neg' {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : b / c < a ↔ c * a < b

theorem lt_div_iff_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : a < b / c ↔ b < a * c

theorem lt_div_iff_of_neg' {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : a < b / c ↔ b < c * a

theorem div_le_one_of_ge {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a

theorem inv_le_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a⁻¹ ≤ b ↔ b⁻¹ ≤ a

theorem le_inv_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a ≤ b⁻¹ ↔ b ≤ a⁻¹

theorem inv_lt_inv_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a⁻¹ < b⁻¹ ↔ b < a

theorem inv_lt_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a⁻¹ < b ↔ b⁻¹ < a

theorem lt_inv_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a < b⁻¹ ↔ b < a⁻¹

Monotonicity results involving inversion

theorem sub_inv_antitoneOn_Ioi {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} : AntitoneOn (fun (x : α) => (x - c)⁻¹) (Set.Ioi c)

theorem sub_inv_antitoneOn_Iio {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} : AntitoneOn (fun (x : α) => (x - c)⁻¹) (Set.Iio c)

theorem sub_inv_antitoneOn_Icc_right {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (ha : c < a) : AntitoneOn (fun (x : α) => (x - c)⁻¹) (Set.Icc a b)

theorem sub_inv_antitoneOn_Icc_left {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (ha : b < c) : AntitoneOn (fun (x : α) => (x - c)⁻¹) (Set.Icc a b)

theorem inv_antitoneOn_Ioi {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] : AntitoneOn (fun (x : α) => x⁻¹) (Set.Ioi 0)

theorem inv_antitoneOn_Iio {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] : AntitoneOn (fun (x : α) => x⁻¹) (Set.Iio 0)

theorem inv_antitoneOn_Icc_right {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) : AntitoneOn (fun (x : α) => x⁻¹) (Set.Icc a b)

theorem inv_antitoneOn_Icc_left {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : c ≤ 0) (h : b ≤ a) : a / c ≤ b / c

theorem div_lt_div_of_neg_of_lt {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) (h : b < a) : a / c < b / c

theorem div_le_div_right_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (hc : c < 0) : a / c ≤ b / c ↔ b ≤ a

theorem div_lt_div_right_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) : 1 ≤ a / b ↔ a ≤ b

theorem div_le_one_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) : a / b ≤ 1 ↔ b ≤ a

theorem one_lt_div_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) : 1 < a / b ↔ a < b

theorem div_lt_one_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) : a / b < 1 ↔ b < a

theorem one_div_le_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : 1 / a ≤ b ↔ 1 / b ≤ a

theorem one_div_lt_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : 1 / a < b ↔ 1 / b < a

theorem le_one_div_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a ≤ 1 / b ↔ b ≤ 1 / a

theorem lt_one_div_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) : a < 1 / b ↔ b < 1 / a

theorem one_lt_div_iff {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

theorem one_le_div_iff {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

theorem div_lt_one_iff {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} : a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

theorem div_le_one_iff {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) (h : 1 / a < 1 / b) : b < a

theorem one_div_le_one_div_of_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (h1 : a < 0) (h2 : -1 < a) : 1 / a < -1

theorem one_div_le_neg_one {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (h1 : a < 0) (h2 : -1 ≤ a) : 1 / a ≤ -1

Results about halving

theorem sub_self_div_two {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) : a - a / 2 = a / 2

theorem div_two_sub_self {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) : a / 2 - a = -(a / 2)

theorem add_sub_div_two_lt {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h : a < b) : a + (b - a) / 2 < b

theorem sub_one_div_inv_le_two {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (a2 : 2 ≤ a) : (1 - 1 / a)⁻¹ ≤ 2

An inequality involving 2.

Results about IsLUB

theorem IsLUB.mul_left {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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_lt_div_of_mul_sub_mul_div_neg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) : (a * d - b * c) / (c * d) < 0 → a / c < b / d

Alias of the forward direction of mul_sub_mul_div_mul_neg_iff.

theorem mul_sub_mul_div_mul_nonpos {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {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 div_le_div_of_mul_sub_mul_div_nonpos {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) : (a * d - b * c) / (c * d) ≤ 0 → a / c ≤ b / d

Alias of the forward direction of mul_sub_mul_div_mul_nonpos_iff.

theorem exists_add_lt_and_pos_of_lt {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h : b < a) : ∃ (c : α), b + c < a ∧ 0 < c

theorem le_of_forall_sub_le {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (h : ∀ ε > 0, b - ε ≤ a) : b ≤ a

theorem le_mul_of_forall_lt₀ {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b

theorem mul_le_of_forall_lt_of_nonneg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b c : α} (ha : 0 ≤ a) (hc : 0 ≤ c) (h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c) : a * b ≤ c

theorem mul_self_inj_of_nonneg {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} (a0 : 0 ≤ a) (b0 : 0 ≤ b) : a * a = b * b ↔ a = b

theorem min_div_div_right_of_nonpos {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} (hc : c ≤ 0) (a b : α) : a / c ⊓ b / c = (a ⊔ b) / c

theorem max_div_div_right_of_nonpos {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} (hc : c ≤ 0) (a b : α) : a / c ⊔ b / c = (a ⊓ b) / c

theorem abs_inv {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) : |a⁻¹| = |a|⁻¹

theorem abs_div {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a b : α) : |a / b| = |a| / |b|

theorem abs_one_div {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) : |1 / a| = 1 / |a|

theorem uniform_continuous_npow_on_bounded {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (B : α) {ε : α} (hε : 0 < ε) (n : ℕ) : ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

def Mathlib.Meta.Positivity.evalDiv : PositivityExt

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.

def Mathlib.Meta.Positivity.evalInv : PositivityExt

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.

def Mathlib.Meta.Positivity.evalPowZeroInt : PositivityExt

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

Equations

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