Lemmas about (linear) ordered (semi)fields

Relating one division and involving 1

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

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

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

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

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

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

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

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

theorem lt_one_div {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {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 α] [PartialOrder α] [PosMulReflectLT α] {a b : α} (b0 : 0 < b) : b < a → 1 < a / b

theorem Bound.div_lt_one_of_pos_of_lt {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {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 α] [PartialOrder α] [PosMulReflectLT α] {a b : α} (ha : 0 < a) (h : a ≤ b) : 1 / b ≤ 1 / a

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

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

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

theorem div_le_self {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α] (ha : 0 ≤ a) (hb : 1 ≤ b) : a / b ≤ a

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

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

theorem one_le_one_div {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α] (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 α] [PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α] (h : 0 < a) : 0 < a / 2

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

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of half_le_self_iff.

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

Alias of half_lt_self.

---

Alias of the reverse direction of half_lt_self_iff.

theorem one_half_lt_one {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] : 1 / 2 < 1

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

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

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

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

Miscellaneous lemmas

@[simp]

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

@[simp]

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

theorem div_mul_le_div_mul_of_div_le_div {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a b c d e : α} [IsStrictOrderedRing α] (h : a / b ≤ c / d) (he : 0 ≤ e) : a / (b * e) ≤ c / (d * e)

theorem mul_le_mul_of_mul_div_le {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a b c d : α} (h : a * (b / c) ≤ d) (hc : 0 < c) : b * a ≤ d * c

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

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

theorem Monotone.div_const {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {β : 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 α] [PartialOrder α] [PosMulReflectLT α] [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 α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] : DenselyOrdered α

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

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

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

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

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

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

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

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

theorem inv_pow_strictAnti {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α] (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 * ε

theorem div_nat_le_self_of_nonnneg {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α] (ha : 0 ≤ a) (n : ℕ) : a / ↑n ≤ a

theorem div_nat_lt_self_of_pos_of_two_le {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α] (ha : 0 < a) {n : ℕ} (hn : 2 ≤ n) : a / ↑n < a

Results about IsGLB

theorem IsGLB.mul_left {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α] {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 α] [PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α] {s : Set α} (ha : 0 ≤ a) (hs : IsGLB s b) : IsGLB ((fun (b : α) => b * a) '' s) (b * a)

Results about IsLUB

theorem IsLUB.mul_left {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α] {s : Set α} (ha : 0 ≤ a) (hs : IsLUB s b) : IsLUB ((fun (b : α) => a * b) '' s) (a * b)

theorem IsLUB.mul_right {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α] {s : Set α} (ha : 0 ≤ a) (hs : IsLUB s b) : IsLUB ((fun (b : α) => b * a) '' s) (b * a)

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

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

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

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

Lemmas about pos, nonneg, nonpos, neg

theorem inv_lt_zero' {α : Type u_2} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a : α} : a⁻¹ < 0 ↔ a < 0

A version of inv_lt_zero which holds with different assumptions. In particular, the type must be a field, not just a GroupWithZero, but the order assumptions replace LinearOrder and PosMulMono with PartialOrder, IsStrictOrderedRing and PosMulReflectLT. Thus neither version is more general than the other. This one applies, for instance, to ℂ.

theorem inv_nonpos' {α : Type u_2} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a : α} : a⁻¹ ≤ 0 ↔ a ≤ 0

A version of inv_nonpos which holds with different assumptions. In particular, the type must be a field, not just a GroupWithZero, but the order assumptions replace LinearOrder and PosMulMono with PartialOrder, IsStrictOrderedRing and PosMulReflectLT. Thus neither version is more general than the other. This one applies, for instance, to ℂ.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem lt_inv_of_neg {α : Type u_2} [Field α] [PartialOrder α] [PosMulReflectLT α] [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 α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {c : α} : AntitoneOn (fun (x : α) => (x - c)⁻¹) (Set.Ioi c)

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

theorem sub_inv_antitoneOn_Icc_right {α : Type u_2} [Field α] [PartialOrder α] [PosMulReflectLT α] [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 α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (ha : b < c) : AntitoneOn (fun (x : α) => (x - c)⁻¹) (Set.Icc a b)

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

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

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

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

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

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

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

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

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

Relating two divisions, involving 1

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

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

Results about halving

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

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

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

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

An inequality involving 2.

Miscellaneous lemmas

theorem mul_sub_mul_div_mul_neg_iff {α : Type u_2} [Field α] [PartialOrder α] [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 α] [PartialOrder α] [IsStrictOrderedRing α] {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} [Field α] [PartialOrder α] [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_neg {α : Type u_2} [Field α] [PartialOrder α] [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_le_div_of_mul_sub_mul_div_nonpos {α : Type u_2} [Field α] [PartialOrder α] [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 mul_sub_mul_div_mul_nonpos {α : Type u_2} [Field α] [PartialOrder α] [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 exists_add_lt_and_pos_of_lt {α : Type u_2} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (h : b < a) : ∃ (c : α), b + c < a ∧ 0 < c

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 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

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_4} [CommRing α] [NoZeroDivisors α] [PartialOrder α] [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 : α) : min (a / c) (b / c) = max a b / c

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

@[simp]

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| < ε

theorem two_mul_le_add_mul_sq {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b ε : α} (hε : 0 < ε) : 2 * a * b ≤ ε * a ^ 2 + ε⁻¹ * b ^ 2

theorem Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg {α : Type u_4} [GroupWithZero α] [PartialOrder α] {a b : α} [PosMulReflectLT α] (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a / b

theorem Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos {α : Type u_4} [GroupWithZero α] [PartialOrder α] {a b : α} [PosMulReflectLT α] (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a / b

theorem Mathlib.Meta.Positivity.div_ne_zero_of_pos_of_ne_zero {α : Type u_4} [GroupWithZero α] [PartialOrder α] {a b : α} (ha : 0 < a) (hb : b ≠ 0) : a / b ≠ 0

theorem Mathlib.Meta.Positivity.div_ne_zero_of_ne_zero_of_pos {α : Type u_4} [GroupWithZero α] [PartialOrder α] {a b : α} (ha : a ≠ 0) (hb : 0 < b) : a / b ≠ 0

theorem Mathlib.Meta.Positivity.zpow_zero_pos {α : Type u_5} [Semifield α] [PartialOrder α] [IsStrictOrderedRing α] (a : α) : 0 < a ^ 0

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.