mathlib documentation

algebra.order.monoid_lemmas_zero_lt

Multiplication by ·positive· elements is monotonic #

Let α be a type with < and 0. We use the type {x : α // 0 < x} of positive elements of α to prove results about monotonicity of multiplication. We also introduce the local notation α>0 for the subtype {x : α // 0 < x}:

If the type α also has a multiplication, then we combine this with (contravariant_) covariant_classes to assume that multiplication by positive elements is (strictly) monotone on a mul_zero_class, monoid_with_zero,... More specifically, we use extensively the following typeclasses:

Formalization comments #

We use α>0 = {x : α // 0 < x} with a strict inequality since in most cases what happens with 0 is clear. This creates a few bumps in the first couple of proofs, where we have to split cases on whether an element is 0 or not, but goes smoothly after that. A further advantage is that we only introduce notation for the positive elements and we do not need also the non-negative ones.

Some lemmas for partial_order also have a variant for preorder, where the preorder version has stronger hypotheses. In this case we put the preorder lemma in the preorder namespace.

def zero_lt.pos_mul_strict_mono (X : Type u) [has_mul X] [has_zero X] [has_lt X] :
Prop

zero_lt.pos_mul_strict_mono α is an abbreviation for covariant_class α>0 α (λ x y, x * y) (<), expressing that multiplication by positive elements on the left is strictly monotone.

def zero_lt.mul_pos_strict_mono (X : Type u) [has_mul X] [has_zero X] [has_lt X] :
Prop

zero_lt.mul_pos_strict_mono α is an abbreviation for covariant_class α>0 α (λ x y, y * x) (<), expressing that multiplication by positive elements on the right is strictly monotone.

def zero_lt.pos_mul_reflect_lt (X : Type u) [has_mul X] [has_zero X] [has_lt X] :
Prop

zero_lt.pos_mul_reflect_lt α is an abbreviation for contravariant_class α>0 α (λ x y, x * y) (<), expressing that multiplication by positive elements on the left is strictly reverse monotone.

def zero_lt.mul_pos_reflect_lt (X : Type u) [has_mul X] [has_zero X] [has_lt X] :
Prop

zero_lt.mul_pos_reflect_lt α is an abbreviation for contravariant_class α>0 α (λ x y, y * x) (<), expressing that multiplication by positive elements on the right is strictly reverse monotone.

def zero_lt.pos_mul_mono (X : Type u_1) [has_mul X] [has_zero X] [has_lt X] [has_le X] :
Prop

zero_lt.pos_mul_mono α is an abbreviation for covariant_class α>0 α (λ x y, x * y) (≤), expressing that multiplication by positive elements on the left is monotone.

def zero_lt.mul_pos_mono (X : Type u_1) [has_mul X] [has_zero X] [has_lt X] [has_le X] :
Prop

zero_lt.mul_pos_mono α is an abbreviation for covariant_class α>0 α (λ x y, y * x) (≤), expressing that multiplication by positive elements on the right is monotone.

def zero_lt.pos_mul_mono_rev (X : Type u_1) [has_mul X] [has_zero X] [has_lt X] [has_le X] :
Prop

zero_lt.pos_mul_mono_rev α is an abbreviation for contravariant_class α>0 α (λ x y, x * y) (≤), expressing that multiplication by positive elements on the left is reverse monotone.

def zero_lt.mul_pos_mono_rev (X : Type u_1) [has_mul X] [has_zero X] [has_lt X] [has_le X] :
Prop

zero_lt.mul_pos_mono_rev α is an abbreviation for contravariant_class α>0 α (λ x y, y * x) (≤), expressing that multiplication by positive elements on the right is reverse monotone.

theorem zero_lt.mul_lt_mul_left' {α : Type u} {a b c : α} [has_mul α] [has_zero α] [has_lt α] [zero_lt.pos_mul_strict_mono α] (bc : b < c) (a0 : 0 < a) :
a * b < a * c
theorem zero_lt.mul_lt_mul_right' {α : Type u} {a b c : α} [has_mul α] [has_zero α] [has_lt α] [zero_lt.mul_pos_strict_mono α] (bc : b < c) (a0 : 0 < a) :
b * a < c * a
theorem zero_lt.lt_of_mul_lt_mul_left' {α : Type u} {a b c : α} [has_mul α] [has_zero α] [has_lt α] [zero_lt.pos_mul_reflect_lt α] (bc : a * b < a * c) (a0 : 0 < a) :
b < c
theorem zero_lt.lt_of_mul_lt_mul_right' {α : Type u} {a b c : α} [has_mul α] [has_zero α] [has_lt α] [zero_lt.mul_pos_reflect_lt α] (bc : b * a < c * a) (a0 : 0 < a) :
b < c
@[simp]
theorem zero_lt.mul_lt_mul_iff_left {α : Type u} {a b c : α} [has_mul α] [has_zero α] [has_lt α] [zero_lt.pos_mul_strict_mono α] [zero_lt.pos_mul_reflect_lt α] (a0 : 0 < a) :
a * b < a * c b < c
@[simp]
theorem zero_lt.mul_lt_mul_iff_right {α : Type u} {a b c : α} [has_mul α] [has_zero α] [has_lt α] [zero_lt.mul_pos_strict_mono α] [zero_lt.mul_pos_reflect_lt α] (a0 : 0 < a) :
b * a < c * a b < c
theorem zero_lt.mul_le_mul_left' {α : Type u} {a b c : α} [has_mul α] [has_zero α] [has_lt α] [has_le α] [zero_lt.pos_mul_mono α] (bc : b c) (a0 : 0 < a) :
a * b a * c
theorem zero_lt.mul_le_mul_right' {α : Type u} {a b c : α} [has_mul α] [has_zero α] [has_lt α] [has_le α] [zero_lt.mul_pos_mono α] (bc : b c) (a0 : 0 < a) :
b * a c * a
theorem zero_lt.le_of_mul_le_mul_left' {α : Type u} {a b c : α} [has_mul α] [has_zero α] [has_lt α] [has_le α] [zero_lt.pos_mul_mono_rev α] (bc : a * b a * c) (a0 : 0 < a) :
b c
theorem zero_lt.le_of_mul_le_mul_right' {α : Type u} {a b c : α} [has_mul α] [has_zero α] [has_lt α] [has_le α] [zero_lt.mul_pos_mono_rev α] (bc : b * a c * a) (a0 : 0 < a) :
b c
@[simp]
theorem zero_lt.mul_le_mul_iff_left {α : Type u} {a b c : α} [has_mul α] [has_zero α] [has_lt α] [has_le α] [zero_lt.pos_mul_mono α] [zero_lt.pos_mul_mono_rev α] (a0 : 0 < a) :
a * b a * c b c
@[simp]
theorem zero_lt.mul_le_mul_iff_right {α : Type u} {a b c : α} [has_mul α] [has_zero α] [has_lt α] [has_le α] [zero_lt.mul_pos_mono α] [zero_lt.mul_pos_mono_rev α] (a0 : 0 < a) :
b * a c * a b c
theorem zero_lt.preorder.mul_le_mul_of_le_of_le {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] [zero_lt.mul_pos_mono α] (h₁ : a b) (h₂ : c d) (a0 : 0 < a) (d0 : 0 < d) :
a * c b * d
theorem zero_lt.preorder.mul_le_mul_of_le_of_le' {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] [zero_lt.mul_pos_mono α] (h₁ : a b) (h₂ : c d) (b0 : 0 < b) (c0 : 0 < c) :
a * c b * d
theorem zero_lt.mul_lt_mul_of_le_of_lt {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] [zero_lt.mul_pos_mono α] (h₁ : a b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 < d) :
a * c < b * d
theorem zero_lt.mul_lt_mul_of_le_of_lt' {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] [zero_lt.mul_pos_mono α] (h₁ : a b) (h₂ : c < d) (b0 : 0 < b) (c0 : 0 < c) :
a * c < b * d
theorem zero_lt.mul_lt_mul_of_lt_of_le {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] [zero_lt.mul_pos_strict_mono α] (h₁ : a < b) (h₂ : c d) (a0 : 0 < a) (d0 : 0 < d) :
a * c < b * d
theorem zero_lt.mul_lt_mul_of_lt_of_le' {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] [zero_lt.mul_pos_strict_mono α] (h₁ : a < b) (h₂ : c d) (b0 : 0 < b) (c0 : 0 < c) :
a * c < b * d
theorem zero_lt.mul_lt_mul_of_lt_of_lt {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] [zero_lt.mul_pos_strict_mono α] (h₁ : a < b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 < d) :
a * c < b * d
theorem zero_lt.mul_lt_mul_of_lt_of_lt' {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] [zero_lt.mul_pos_strict_mono α] (h₁ : a < b) (h₂ : c < d) (b0 : 0 < b) (c0 : 0 < c) :
a * c < b * d
theorem zero_lt.preorder.mul_le_of_mul_le_left {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (h : a * b c) (hle : d b) (a0 : 0 < a) :
a * d c
theorem zero_lt.mul_lt_of_mul_lt_left {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (h : a * b < c) (hle : d b) (a0 : 0 < a) :
a * d < c
theorem zero_lt.preorder.le_mul_of_le_mul_left {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (h : a b * c) (hle : c d) (b0 : 0 < b) :
a b * d
theorem zero_lt.lt_mul_of_lt_mul_left {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (h : a < b * c) (hle : c d) (b0 : 0 < b) :
a < b * d
theorem zero_lt.preorder.mul_le_of_mul_le_right {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (h : a * b c) (hle : d a) (b0 : 0 < b) :
d * b c
theorem zero_lt.mul_lt_of_mul_lt_right {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (h : a * b < c) (hle : d a) (b0 : 0 < b) :
d * b < c
theorem zero_lt.preorder.le_mul_of_le_mul_right {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (h : a b * c) (hle : b d) (c0 : 0 < c) :
a d * c
theorem zero_lt.lt_mul_of_lt_mul_right {α : Type u} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (h : a < b * c) (hle : b d) (c0 : 0 < c) :
a < d * c
theorem zero_lt.left.mul_pos {α : Type u} {a b : α} [mul_zero_class α] [preorder α] [zero_lt.pos_mul_strict_mono α] (ha : 0 < a) (hb : 0 < b) :
0 < a * b

Assumes left covariance.

theorem zero_lt.mul_neg_of_pos_of_neg {α : Type u} {a b : α} [mul_zero_class α] [preorder α] [zero_lt.pos_mul_strict_mono α] (ha : 0 < a) (hb : b < 0) :
a * b < 0
theorem zero_lt.right.mul_pos {α : Type u} {a b : α} [mul_zero_class α] [preorder α] [zero_lt.mul_pos_strict_mono α] (ha : 0 < a) (hb : 0 < b) :
0 < a * b

Assumes right covariance.

theorem zero_lt.mul_neg_of_neg_of_pos {α : Type u} {a b : α} [mul_zero_class α] [preorder α] [zero_lt.mul_pos_strict_mono α] (ha : a < 0) (hb : 0 < b) :
a * b < 0
theorem zero_lt.mul_le_mul_left {α : Type u} {a b c : α} [mul_zero_class α] [partial_order α] [zero_lt.pos_mul_mono α] (bc : b c) (a0 : 0 a) :
a * b a * c
theorem zero_lt.mul_le_mul_right {α : Type u} {a b c : α} [mul_zero_class α] [partial_order α] [zero_lt.mul_pos_mono α] (bc : b c) (a0 : 0 a) :
b * a c * a
theorem zero_lt.left.mul_nonneg {α : Type u} {a b : α} [mul_zero_class α] [partial_order α] [zero_lt.pos_mul_mono α] (ha : 0 a) (hb : 0 b) :
0 a * b

Assumes left covariance.

theorem zero_lt.mul_nonpos_of_nonneg_of_nonpos {α : Type u} {a b : α} [mul_zero_class α] [partial_order α] [zero_lt.pos_mul_mono α] (ha : 0 a) (hb : b 0) :
a * b 0
theorem zero_lt.right.mul_nonneg {α : Type u} {a b : α} [mul_zero_class α] [partial_order α] [zero_lt.mul_pos_mono α] (ha : 0 a) (hb : 0 b) :
0 a * b

Assumes right covariance.

theorem zero_lt.mul_nonpos_of_nonpos_of_nonneg {α : Type u} {a b : α} [mul_zero_class α] [partial_order α] [zero_lt.mul_pos_mono α] (ha : a 0) (hb : 0 b) :
a * b 0
theorem zero_lt.lt_of_mul_lt_mul_left {α : Type u} {a b c : α} [mul_zero_class α] [partial_order α] [zero_lt.pos_mul_reflect_lt α] (bc : a * b < a * c) (a0 : 0 a) :
b < c
theorem zero_lt.pos_of_mul_pos_left {α : Type u} {a b : α} [mul_zero_class α] [partial_order α] [zero_lt.pos_mul_reflect_lt α] (h : 0 < a * b) (ha : 0 a) :
0 < b
theorem zero_lt.lt_of_mul_lt_mul_right {α : Type u} {a b c : α} [mul_zero_class α] [partial_order α] [zero_lt.mul_pos_reflect_lt α] (bc : b * a < c * a) (a0 : 0 a) :
b < c
theorem zero_lt.pos_of_mul_pos_right {α : Type u} {a b : α} [mul_zero_class α] [partial_order α] [zero_lt.mul_pos_reflect_lt α] (h : 0 < a * b) (hb : 0 b) :
0 < a
theorem zero_lt.pos_iff_pos_of_mul_pos {α : Type u} {a b : α} [mul_zero_class α] [partial_order α] [zero_lt.pos_mul_reflect_lt α] [zero_lt.mul_pos_reflect_lt α] (hab : 0 < a * b) :
0 < a 0 < b
theorem zero_lt.mul_le_mul_of_le_of_le {α : Type u} {a b c d : α} [mul_zero_class α] [partial_order α] [zero_lt.pos_mul_mono α] [zero_lt.mul_pos_mono α] (h₁ : a b) (h₂ : c d) (a0 : 0 a) (d0 : 0 d) :
a * c b * d
theorem zero_lt.mul_le_mul_of_le_of_le' {α : Type u} {a b c d : α} [mul_zero_class α] [partial_order α] [zero_lt.pos_mul_mono α] [zero_lt.mul_pos_mono α] (h₁ : a b) (h₂ : c d) (b0 : 0 b) (c0 : 0 c) :
a * c b * d
theorem zero_lt.mul_le_of_mul_le_left {α : Type u} {a b c d : α} [mul_zero_class α] [partial_order α] [zero_lt.pos_mul_mono α] (h : a * b c) (hle : d b) (a0 : 0 a) :
a * d c
theorem zero_lt.le_mul_of_le_mul_left {α : Type u} {a b c d : α} [mul_zero_class α] [partial_order α] [zero_lt.pos_mul_mono α] (h : a b * c) (hle : c d) (b0 : 0 b) :
a b * d
theorem zero_lt.mul_le_of_mul_le_right {α : Type u} {a b c d : α} [mul_zero_class α] [partial_order α] [zero_lt.mul_pos_mono α] (h : a * b c) (hle : d a) (b0 : 0 b) :
d * b c
theorem zero_lt.le_mul_of_le_mul_right {α : Type u} {a b c d : α} [mul_zero_class α] [partial_order α] [zero_lt.mul_pos_mono α] (h : a b * c) (hle : b d) (c0 : 0 c) :
a d * c
theorem zero_lt.mul_left_cancel_iff {α : Type u} {a b c : α} [mul_zero_class α] [partial_order α] [zero_lt.pos_mul_mono_rev α] (a0 : 0 < a) :
a * b = a * c b = c
theorem zero_lt.mul_right_cancel_iff {α : Type u} {a b c : α} [mul_zero_class α] [partial_order α] [zero_lt.mul_pos_mono_rev α] (b0 : 0 < b) :
a * b = c * b a = c
theorem zero_lt.mul_eq_mul_iff_eq_and_eq {α : Type u} {a b c d : α} [mul_zero_class α] [partial_order α] [zero_lt.pos_mul_strict_mono α] [zero_lt.mul_pos_strict_mono α] [zero_lt.pos_mul_mono_rev α] [zero_lt.mul_pos_mono_rev α] (hac : a b) (hbd : c d) (a0 : 0 < a) (d0 : 0 < d) :
a * c = b * d a = b c = d
theorem zero_lt.mul_eq_mul_iff_eq_and_eq' {α : Type u} {a b c d : α} [mul_zero_class α] [partial_order α] [zero_lt.pos_mul_strict_mono α] [zero_lt.mul_pos_strict_mono α] [zero_lt.pos_mul_mono_rev α] [zero_lt.mul_pos_mono_rev α] (hac : a b) (hbd : c d) (b0 : 0 < b) (c0 : 0 < c) :
a * c = b * d a = b c = d
theorem zero_lt.pos_and_pos_or_neg_and_neg_of_mul_pos {α : Type u} {a b : α} [mul_zero_class α] [linear_order α] [zero_lt.pos_mul_mono α] [zero_lt.mul_pos_mono α] (hab : 0 < a * b) :
0 < a 0 < b a < 0 b < 0
theorem zero_lt.neg_of_mul_pos_left {α : Type u} {a b : α} [mul_zero_class α] [linear_order α] [zero_lt.pos_mul_mono α] [zero_lt.mul_pos_mono α] (h : 0 < a * b) (ha : a 0) :
b < 0
theorem zero_lt.neg_of_mul_pos_right {α : Type u} {a b : α} [mul_zero_class α] [linear_order α] [zero_lt.pos_mul_mono α] [zero_lt.mul_pos_mono α] (h : 0 < a * b) (ha : b 0) :
a < 0
theorem zero_lt.neg_iff_neg_of_mul_pos {α : Type u} {a b : α} [mul_zero_class α] [linear_order α] [zero_lt.pos_mul_mono α] [zero_lt.mul_pos_mono α] (hab : 0 < a * b) :
a < 0 b < 0
theorem zero_lt.left.neg_of_mul_neg_left {α : Type u} {a b : α} [mul_zero_class α] [linear_order α] [zero_lt.pos_mul_mono α] (h : a * b < 0) (h1 : 0 a) :
b < 0
theorem zero_lt.right.neg_of_mul_neg_left {α : Type u} {a b : α} [mul_zero_class α] [linear_order α] [zero_lt.mul_pos_mono α] (h : a * b < 0) (h1 : 0 a) :
b < 0
theorem zero_lt.left.neg_of_mul_neg_right {α : Type u} {a b : α} [mul_zero_class α] [linear_order α] [zero_lt.pos_mul_mono α] (h : a * b < 0) (h1 : 0 b) :
a < 0
theorem zero_lt.right.neg_of_mul_neg_right {α : Type u} {a b : α} [mul_zero_class α] [linear_order α] [zero_lt.mul_pos_mono α] (h : a * b < 0) (h1 : 0 b) :
a < 0

Lemmas of the form a ≤ a * b ↔ 1 ≤ b and a * b ≤ a ↔ b ≤ 1, which assume left covariance.

@[simp]
theorem zero_lt.le_mul_iff_one_le_right {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] [zero_lt.pos_mul_mono_rev α] (a0 : 0 < a) :
a a * b 1 b
@[simp]
theorem zero_lt.lt_mul_iff_one_lt_right {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] [zero_lt.pos_mul_reflect_lt α] (a0 : 0 < a) :
a < a * b 1 < b
@[simp]
theorem zero_lt.mul_le_iff_le_one_right {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] [zero_lt.pos_mul_mono_rev α] (a0 : 0 < a) :
a * b a b 1
@[simp]
theorem zero_lt.mul_lt_iff_lt_one_right {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] [zero_lt.pos_mul_reflect_lt α] (a0 : 0 < a) :
a * b < a b < 1

Lemmas of the form a ≤ b * a ↔ 1 ≤ b and a * b ≤ b ↔ a ≤ 1, which assume right covariance.

@[simp]
theorem zero_lt.le_mul_iff_one_le_left {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] [zero_lt.mul_pos_mono_rev α] (a0 : 0 < a) :
a b * a 1 b
@[simp]
theorem zero_lt.lt_mul_iff_one_lt_left {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_strict_mono α] [zero_lt.mul_pos_reflect_lt α] (a0 : 0 < a) :
a < b * a 1 < b
@[simp]
theorem zero_lt.mul_le_iff_le_one_left {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] [zero_lt.mul_pos_mono_rev α] (b0 : 0 < b) :
a * b b a 1
@[simp]
theorem zero_lt.mul_lt_iff_lt_one_left {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_strict_mono α] [zero_lt.mul_pos_reflect_lt α] (b0 : 0 < b) :
a * b < b a < 1

Lemmas of the form b ≤ c → a ≤ 1 → 0 < b → b * a ≤ c, which assume left covariance.

theorem zero_lt.preorder.mul_le_of_le_of_le_one {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (bc : b c) (ha : a 1) (b0 : 0 < b) :
b * a c
theorem zero_lt.mul_lt_of_le_of_lt_one {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] (bc : b c) (ha : a < 1) (b0 : 0 < b) :
b * a < c
theorem zero_lt.mul_lt_of_lt_of_le_one {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (bc : b < c) (ha : a 1) (b0 : 0 < b) :
b * a < c
theorem zero_lt.mul_lt_of_lt_of_lt_one {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] (bc : b < c) (ha : a < 1) (b0 : 0 < b) :
b * a < c
theorem zero_lt.preorder.left.mul_le_one_of_le_of_le' {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (ha : a 1) (hb : b 1) (a0 : 0 < a) :
a * b 1

Assumes left covariance.

theorem zero_lt.left.mul_lt_one_of_le_of_lt {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] (ha : a 1) (hb : b < 1) (a0 : 0 < a) :
a * b < 1

Assumes left covariance.

theorem zero_lt.left.mul_lt_one_of_lt_of_le {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (ha : a < 1) (hb : b 1) (a0 : 0 < a) :
a * b < 1

Assumes left covariance.

theorem zero_lt.left.mul_lt_one_of_lt_of_lt {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] (ha : a < 1) (hb : b < 1) (a0 : 0 < a) :
a * b < 1

Assumes left covariance.

Lemmas of the form b ≤ c → 1 ≤ a → 0 < c → b ≤ c * a, which assume left covariance.

theorem zero_lt.preorder.le_mul_of_le_of_one_le {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (bc : b c) (ha : 1 a) (c0 : 0 < c) :
b c * a
theorem zero_lt.lt_mul_of_le_of_one_lt {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] (bc : b c) (ha : 1 < a) (c0 : 0 < c) :
b < c * a
theorem zero_lt.lt_mul_of_lt_of_one_le {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (bc : b < c) (ha : 1 a) (c0 : 0 < c) :
b < c * a
theorem zero_lt.lt_mul_of_lt_of_one_lt {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] (bc : b < c) (ha : 1 < a) (c0 : 0 < c) :
b < c * a
theorem zero_lt.preorder.left.one_le_mul_of_le_of_le {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (ha : 1 a) (hb : 1 b) (a0 : 0 < a) :
1 a * b

Assumes left covariance.

theorem zero_lt.left.one_lt_mul_of_le_of_lt {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] (ha : 1 a) (hb : 1 < b) (a0 : 0 < a) :
1 < a * b

Assumes left covariance.

theorem zero_lt.left.one_lt_mul_of_lt_of_le {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (ha : 1 < a) (hb : 1 b) (a0 : 0 < a) :
1 < a * b

Assumes left covariance.

theorem zero_lt.left.one_lt_mul_of_lt_of_lt {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_strict_mono α] (ha : 1 < a) (hb : 1 < b) (a0 : 0 < a) :
1 < a * b

Assumes left covariance.

Lemmas of the form a ≤ 1 → b ≤ c → 0 < b → a * b ≤ c, which assume right covariance.

theorem zero_lt.preorder.mul_le_of_le_one_of_le {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (ha : a 1) (bc : b c) (b0 : 0 < b) :
a * b c
theorem zero_lt.mul_lt_of_lt_one_of_le {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_strict_mono α] (ha : a < 1) (bc : b c) (b0 : 0 < b) :
a * b < c
theorem zero_lt.mul_lt_of_le_one_of_lt {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (ha : a 1) (hb : b < c) (b0 : 0 < b) :
a * b < c
theorem zero_lt.mul_lt_of_lt_one_of_lt {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_strict_mono α] (ha : a < 1) (bc : b < c) (b0 : 0 < b) :
a * b < c
theorem zero_lt.preorder.right.mul_le_one_of_le_of_le {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (ha : a 1) (hb : b 1) (b0 : 0 < b) :
a * b 1

Assumes right covariance.

theorem zero_lt.right.mul_lt_one_of_lt_of_le {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_strict_mono α] (ha : a < 1) (hb : b 1) (b0 : 0 < b) :
a * b < 1

Assumes right covariance.

theorem zero_lt.right.mul_lt_one_of_le_of_lt {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (ha : a 1) (hb : b < 1) (b0 : 0 < b) :
a * b < 1

Assumes right covariance.

theorem zero_lt.right.mul_lt_one_of_lt_of_lt {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_strict_mono α] (ha : a < 1) (hb : b < 1) (b0 : 0 < b) :
a * b < 1

Assumes right covariance.

Lemmas of the form 1 ≤ a → b ≤ c → 0 < c → b ≤ a * c, which assume right covariance.

theorem zero_lt.preorder.le_mul_of_one_le_of_le {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (ha : 1 a) (bc : b c) (c0 : 0 < c) :
b a * c
theorem zero_lt.lt_mul_of_one_lt_of_le {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_strict_mono α] (ha : 1 < a) (bc : b c) (c0 : 0 < c) :
b < a * c
theorem zero_lt.lt_mul_of_one_le_of_lt {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (ha : 1 a) (bc : b < c) (c0 : 0 < c) :
b < a * c
theorem zero_lt.lt_mul_of_one_lt_of_lt {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_strict_mono α] (ha : 1 < a) (bc : b < c) (c0 : 0 < c) :
b < a * c
theorem zero_lt.preorder.right.one_le_mul_of_le_of_le {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (ha : 1 a) (hb : 1 b) (b0 : 0 < b) :
1 a * b

Assumes right covariance.

theorem zero_lt.right.one_lt_mul_of_lt_of_le {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_strict_mono α] (ha : 1 < a) (hb : 1 b) (b0 : 0 < b) :
1 < a * b

Assumes right covariance.

theorem zero_lt.right.one_lt_mul_of_le_of_lt {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (ha : 1 a) (hb : 1 < b) (b0 : 0 < b) :
1 < a * b

Assumes right covariance.

theorem zero_lt.right.one_lt_mul_of_lt_of_lt {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_strict_mono α] (ha : 1 < a) (hb : 1 < b) (b0 : 0 < b) :
1 < a * b

Assumes right covariance.

theorem zero_lt.preorder.mul_le_of_le_one_right {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (h : b 1) (a0 : 0 < a) :
a * b a
theorem zero_lt.preorder.le_mul_of_one_le_right {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (h : 1 b) (a0 : 0 < a) :
a a * b
theorem zero_lt.preorder.mul_le_of_le_one_left {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (h : a 1) (b0 : 0 < b) :
a * b b
theorem zero_lt.preorder.le_mul_of_one_le_left {α : Type u} {a b : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (h : 1 a) (b0 : 0 < b) :
b a * b
theorem zero_lt.preorder.le_of_mul_le_of_one_le_left {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (h : a * b c) (hle : 1 b) (a0 : 0 < a) :
a c
theorem zero_lt.lt_of_mul_lt_of_one_le_left {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (h : a * b < c) (hle : 1 b) (a0 : 0 < a) :
a < c
theorem zero_lt.preorder.le_of_le_mul_of_le_one_left {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (h : a b * c) (hle : c 1) (b0 : 0 < b) :
a b
theorem zero_lt.lt_of_lt_mul_of_le_one_left {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.pos_mul_mono α] (h : a < b * c) (hle : c 1) (b0 : 0 < b) :
a < b
theorem zero_lt.preorder.le_of_mul_le_of_one_le_right {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (h : a * b c) (hle : 1 a) (b0 : 0 < b) :
b c
theorem zero_lt.lt_of_mul_lt_of_one_le_right {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (h : a * b < c) (hle : 1 a) (b0 : 0 < b) :
b < c
theorem zero_lt.le_of_le_mul_of_le_one_right' {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (h : a b * c) (hle : b 1) (c0 : 0 < c) :
a c
theorem zero_lt.lt_of_lt_mul_of_le_one_right {α : Type u} {a b c : α} [mul_one_class α] [has_zero α] [preorder α] [zero_lt.mul_pos_mono α] (h : a < b * c) (hle : b 1) (c0 : 0 < c) :
a < c
theorem zero_lt.exists_square_le' {α : Type u} {a : α} [mul_one_class α] [has_zero α] [linear_order α] [zero_lt.pos_mul_strict_mono α] (a0 : 0 < a) :
∃ (b : α), b * b a
theorem zero_lt.mul_le_of_le_of_le_one {α : Type u} {a b c : α} [mul_zero_one_class α] [partial_order α] [zero_lt.pos_mul_mono α] (bc : b c) (ha : a 1) (b0 : 0 b) :
b * a c
theorem zero_lt.left.mul_le_one_of_le_of_le {α : Type u} {a b : α} [mul_zero_one_class α] [partial_order α] [zero_lt.pos_mul_mono α] (ha : a 1) (hb : b 1) (a0 : 0 a) :
a * b 1

Assumes left covariance.

theorem zero_lt.le_mul_of_le_of_one_le {α : Type u} {a b c : α} [mul_zero_one_class α] [partial_order α] [zero_lt.pos_mul_mono α] (bc : b c) (ha : 1 a) (c0 : 0 c) :
b c * a
theorem zero_lt.left.one_le_mul_of_le_of_le {α : Type u} {a b : α} [mul_zero_one_class α] [partial_order α] [zero_lt.pos_mul_mono α] (ha : 1 a) (hb : 1 b) (a0 : 0 a) :
1 a * b

Assumes left covariance.

theorem zero_lt.mul_le_of_le_one_of_le {α : Type u} {a b c : α} [mul_zero_one_class α] [partial_order α] [zero_lt.mul_pos_mono α] (ha : a 1) (bc : b c) (b0 : 0 b) :
a * b c
theorem zero_lt.right.mul_le_one_of_le_of_le {α : Type u} {a b : α} [mul_zero_one_class α] [partial_order α] [zero_lt.mul_pos_mono α] (ha : a 1) (hb : b 1) (b0 : 0 < b) :
a * b 1

Assumes right covariance.

theorem zero_lt.le_mul_of_one_le_of_le {α : Type u} {a b c : α} [mul_zero_one_class α] [partial_order α] [zero_lt.mul_pos_mono α] (ha : 1 a) (bc : b c) (c0 : 0 c) :
b a * c
theorem zero_lt.right.one_le_mul_of_le_of_le {α : Type u} {a b : α} [mul_zero_one_class α] [partial_order α] [zero_lt.mul_pos_mono α] (ha : 1 a) (hb : 1 b) (b0 : 0 b) :
1 a * b

Assumes right covariance.

theorem zero_lt.mul_le_of_le_one_right {α : Type u} {a b : α} [mul_zero_one_class α] [partial_order α] [zero_lt.pos_mul_mono α] (h : b 1) (a0 : 0 a) :
a * b a
theorem zero_lt.le_mul_of_one_le_right {α : Type u} {a b : α} [mul_zero_one_class α] [partial_order α] [zero_lt.pos_mul_mono α] (h : 1 b) (a0 : 0 a) :
a a * b
theorem zero_lt.mul_le_of_le_one_left {α : Type u} {a b : α} [mul_zero_one_class α] [partial_order α] [zero_lt.mul_pos_mono α] (h : a 1) (b0 : 0 b) :
a * b b
theorem zero_lt.le_mul_of_one_le_left {α : Type u} {a b : α} [mul_zero_one_class α] [partial_order α] [zero_lt.mul_pos_mono α] (h : 1 a) (b0 : 0 b) :
b a * b
theorem zero_lt.le_of_mul_le_of_one_le_left {α : Type u} {a b c : α} [mul_zero_one_class α] [partial_order α] [zero_lt.pos_mul_mono α] (h : a * b c) (hle : 1 b) (a0 : 0 a) :
a c
theorem zero_lt.le_of_le_mul_of_le_one_left {α : Type u} {a b c : α} [mul_zero_one_class α] [partial_order α] [zero_lt.pos_mul_mono α] (h : a b * c) (hle : c 1) (b0 : 0 b) :
a b
theorem zero_lt.le_of_mul_le_of_one_le_right {α : Type u} {a b c : α} [mul_zero_one_class α] [partial_order α] [zero_lt.mul_pos_mono α] (h : a * b c) (hle : 1 a) (b0 : 0 b) :
b c
theorem zero_lt.le_of_le_mul_of_le_one_right {α : Type u} {a b c : α} [mul_zero_one_class α] [partial_order α] [zero_lt.mul_pos_mono α] (h : a b * c) (hle : b 1) (c0 : 0 c) :
a c
theorem zero_lt.exists_square_le {α : Type u} {a : α} [mul_zero_one_class α] [linear_order α] [zero_lt.pos_mul_strict_mono α] (a0 : 0 a) :
∃ (b : α), b * b a