Multiplication by ·positive· elements is monotonic #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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:
- monotone left
-
covariant_class α>0 α (λ x y, x * y) (≤), abbreviatedpos_mul_mono α, expressing that multiplication by positive elements on the left is monotone;
-
covariant_class α>0 α (λ x y, x * y) (<), abbreviatedpos_mul_strict_mono α, expressing that multiplication by positive elements on the left is strictly monotone;
- monotone right
-
covariant_class α>0 α (λ x y, y * x) (≤), abbreviatedmul_pos_mono α, expressing that multiplication by positive elements on the right is monotone;
-
covariant_class α>0 α (λ x y, y * x) (<), abbreviatedmul_pos_strict_mono α, expressing that multiplication by positive elements on the right is strictly monotone.
- reverse monotone left
-
contravariant_class α>0 α (λ x y, x * y) (≤), abbreviatedpos_mul_mono_rev α, expressing that multiplication by positive elements on the left is reverse monotone;
-
contravariant_class α>0 α (λ x y, x * y) (<), abbreviatedpos_mul_reflect_lt α, expressing that multiplication by positive elements on the left is strictly reverse monotone;
- reverse reverse monotone right
-
contravariant_class α>0 α (λ x y, y * x) (≤), abbreviatedmul_pos_mono_rev α, expressing that multiplication by positive elements on the right is reverse monotone;
-
contravariant_class α>0 α (λ x y, y * x) (<), abbreviatedmul_pos_reflect_lt α, expressing that multiplication by positive elements on the right is strictly reverse monotone.
Notation #
The following is local notation in this file:
α≥0:{x : α // 0 ≤ x}α>0:{x : α // 0 < x}
@[reducible]
pos_mul_mono α is an abbreviation for covariant_class α≥0 α (λ x y, x * y) (≤),
expressing that multiplication by nonnegative elements on the left is monotone.
@[reducible]
mul_pos_mono α is an abbreviation for covariant_class α≥0 α (λ x y, y * x) (≤),
expressing that multiplication by nonnegative elements on the right is monotone.
@[reducible]
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.
@[reducible]
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.
@[reducible]
pos_mul_reflect_lt α is an abbreviation for contravariant_class α≥0 α (λ x y, x * y) (<),
expressing that multiplication by nonnegative elements on the left is strictly reverse monotone.
@[reducible]
mul_pos_reflect_lt α is an abbreviation for contravariant_class α≥0 α (λ x y, y * x) (<),
expressing that multiplication by nonnegative elements on the right is strictly reverse monotone.
@[reducible]
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.
@[reducible]
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.
@[protected, instance]
def
pos_mul_mono.to_covariant_class_pos_mul_le
{α : Type u_1}
[has_mul α]
[has_zero α]
[preorder α]
[pos_mul_mono α] :
@[protected, instance]
def
mul_pos_mono.to_covariant_class_pos_mul_le
{α : Type u_1}
[has_mul α]
[has_zero α]
[preorder α]
[mul_pos_mono α] :
@[protected, instance]
def
pos_mul_reflect_lt.to_contravariant_class_pos_mul_lt
{α : Type u_1}
[has_mul α]
[has_zero α]
[preorder α]
[pos_mul_reflect_lt α] :
@[protected, instance]
def
mul_pos_reflect_lt.to_contravariant_class_pos_mul_lt
{α : Type u_1}
[has_mul α]
[has_zero α]
[preorder α]
[mul_pos_reflect_lt α] :
theorem
lt_of_mul_lt_mul_of_nonneg_left
{α : Type u_1}
{a b c : α}
[has_mul α]
[has_zero α]
[preorder α]
[pos_mul_reflect_lt α]
(h : a * b < a * c)
(a0 : 0 ≤ a) :
b < c
Alias of lt_of_mul_lt_mul_left.
theorem
lt_of_mul_lt_mul_of_nonneg_right
{α : Type u_1}
{a b c : α}
[has_mul α]
[has_zero α]
[preorder α]
[mul_pos_reflect_lt α]
(h : b * a < c * a)
(a0 : 0 ≤ a) :
b < c
Alias of lt_of_mul_lt_mul_right.
theorem
le_of_mul_le_mul_of_pos_left
{α : Type u_1}
{a b c : α}
[has_mul α]
[has_zero α]
[preorder α]
[pos_mul_mono_rev α]
(bc : a * b ≤ a * c)
(a0 : 0 < a) :
b ≤ c
Alias of le_of_mul_le_mul_left.
theorem
le_of_mul_le_mul_of_pos_right
{α : Type u_1}
{a b c : α}
[has_mul α]
[has_zero α]
[preorder α]
[mul_pos_mono_rev α]
(bc : b * a ≤ c * a)
(a0 : 0 < a) :
b ≤ c
Alias of le_of_mul_le_mul_right.
@[simp]
theorem
mul_lt_mul_left
{α : Type u_1}
{a b c : α}
[has_mul α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
[pos_mul_reflect_lt α]
(a0 : 0 < a) :
@[simp]
theorem
mul_lt_mul_right
{α : Type u_1}
{a b c : α}
[has_mul α]
[has_zero α]
[preorder α]
[mul_pos_strict_mono α]
[mul_pos_reflect_lt α]
(a0 : 0 < a) :
@[simp]
theorem
mul_le_mul_left
{α : Type u_1}
{a b c : α}
[has_mul α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
[pos_mul_mono_rev α]
(a0 : 0 < a) :
@[simp]
theorem
mul_le_mul_right
{α : Type u_1}
{a b c : α}
[has_mul α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
[mul_pos_mono_rev α]
(a0 : 0 < a) :
theorem
mul_lt_mul_of_pos_of_nonneg
{α : Type u_1}
{a b c d : α}
[has_mul α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
[mul_pos_mono α]
(h₁ : a ≤ b)
(h₂ : c < d)
(a0 : 0 < a)
(d0 : 0 ≤ d) :
theorem
mul_lt_mul_of_le_of_le'
{α : Type u_1}
{a b c d : α}
[has_mul α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
[mul_pos_mono α]
(h₁ : a ≤ b)
(h₂ : c < d)
(b0 : 0 < b)
(c0 : 0 ≤ c) :
theorem
mul_lt_mul_of_nonneg_of_pos
{α : Type u_1}
{a b c d : α}
[has_mul α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
[mul_pos_strict_mono α]
(h₁ : a < b)
(h₂ : c ≤ d)
(a0 : 0 ≤ a)
(d0 : 0 < d) :
theorem
mul_lt_mul_of_le_of_lt'
{α : Type u_1}
{a b c d : α}
[has_mul α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
[mul_pos_strict_mono α]
(h₁ : a < b)
(h₂ : c ≤ d)
(b0 : 0 ≤ b)
(c0 : 0 < c) :
theorem
mul_lt_mul_of_pos_of_pos
{α : Type u_1}
{a b c d : α}
[has_mul α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
[mul_pos_strict_mono α]
(h₁ : a < b)
(h₂ : c < d)
(a0 : 0 < a)
(d0 : 0 < d) :
theorem
mul_lt_mul_of_lt_of_lt'
{α : Type u_1}
{a b c d : α}
[has_mul α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
[mul_pos_strict_mono α]
(h₁ : a < b)
(h₂ : c < d)
(b0 : 0 < b)
(c0 : 0 < c) :
@[protected, instance]
def
pos_mul_strict_mono.to_pos_mul_mono_rev
{α : Type u_1}
[has_mul α]
[has_zero α]
[linear_order α]
[pos_mul_strict_mono α] :
@[protected, instance]
def
mul_pos_strict_mono.to_mul_pos_mono_rev
{α : Type u_1}
[has_mul α]
[has_zero α]
[linear_order α]
[mul_pos_strict_mono α] :
theorem
pos_mul_mono_rev.to_pos_mul_strict_mono
{α : Type u_1}
[has_mul α]
[has_zero α]
[linear_order α]
[pos_mul_mono_rev α] :
theorem
mul_pos_mono_rev.to_mul_pos_strict_mono
{α : Type u_1}
[has_mul α]
[has_zero α]
[linear_order α]
[mul_pos_mono_rev α] :
theorem
pos_mul_strict_mono_iff_pos_mul_mono_rev
{α : Type u_1}
[has_mul α]
[has_zero α]
[linear_order α] :
theorem
mul_pos_strict_mono_iff_mul_pos_mono_rev
{α : Type u_1}
[has_mul α]
[has_zero α]
[linear_order α] :
theorem
pos_mul_reflect_lt.to_pos_mul_mono
{α : Type u_1}
[has_mul α]
[has_zero α]
[linear_order α]
[pos_mul_reflect_lt α] :
theorem
mul_pos_reflect_lt.to_mul_pos_mono
{α : Type u_1}
[has_mul α]
[has_zero α]
[linear_order α]
[mul_pos_reflect_lt α] :
theorem
pos_mul_mono.to_pos_mul_reflect_lt
{α : Type u_1}
[has_mul α]
[has_zero α]
[linear_order α]
[pos_mul_mono α] :
theorem
mul_pos_mono.to_mul_pos_reflect_lt
{α : Type u_1}
[has_mul α]
[has_zero α]
[linear_order α]
[mul_pos_mono α] :
theorem
pos_mul_mono_iff_pos_mul_reflect_lt
{α : Type u_1}
[has_mul α]
[has_zero α]
[linear_order α] :
theorem
mul_pos_mono_iff_mul_pos_reflect_lt
{α : Type u_1}
[has_mul α]
[has_zero α]
[linear_order α] :
theorem
left.mul_pos
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[pos_mul_strict_mono α]
(ha : 0 < a)
(hb : 0 < b) :
Assumes left covariance.
theorem
mul_pos
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[pos_mul_strict_mono α]
(ha : 0 < a)
(hb : 0 < b) :
Alias of left.mul_pos.
theorem
mul_neg_of_pos_of_neg
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[pos_mul_strict_mono α]
(ha : 0 < a)
(hb : b < 0) :
@[simp]
theorem
zero_lt_mul_left
{α : Type u_1}
{b c : α}
[mul_zero_class α]
[preorder α]
[pos_mul_strict_mono α]
[pos_mul_reflect_lt α]
(h : 0 < c) :
theorem
right.mul_pos
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[mul_pos_strict_mono α]
(ha : 0 < a)
(hb : 0 < b) :
Assumes right covariance.
theorem
mul_neg_of_neg_of_pos
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[mul_pos_strict_mono α]
(ha : a < 0)
(hb : 0 < b) :
@[simp]
theorem
zero_lt_mul_right
{α : Type u_1}
{b c : α}
[mul_zero_class α]
[preorder α]
[mul_pos_strict_mono α]
[mul_pos_reflect_lt α]
(h : 0 < c) :
theorem
left.mul_nonneg
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[pos_mul_mono α]
(ha : 0 ≤ a)
(hb : 0 ≤ b) :
Assumes left covariance.
theorem
mul_nonneg
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[pos_mul_mono α]
(ha : 0 ≤ a)
(hb : 0 ≤ b) :
Alias of left.mul_nonneg.
theorem
mul_nonpos_of_nonneg_of_nonpos
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[pos_mul_mono α]
(ha : 0 ≤ a)
(hb : b ≤ 0) :
theorem
right.mul_nonneg
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[mul_pos_mono α]
(ha : 0 ≤ a)
(hb : 0 ≤ b) :
Assumes right covariance.
theorem
mul_nonpos_of_nonpos_of_nonneg
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[mul_pos_mono α]
(ha : a ≤ 0)
(hb : 0 ≤ b) :
theorem
pos_of_mul_pos_right
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[pos_mul_reflect_lt α]
(h : 0 < a * b)
(ha : 0 ≤ a) :
0 < b
theorem
pos_of_mul_pos_left
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[mul_pos_reflect_lt α]
(h : 0 < a * b)
(hb : 0 ≤ b) :
0 < a
theorem
pos_iff_pos_of_mul_pos
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[pos_mul_reflect_lt α]
[mul_pos_reflect_lt α]
(hab : 0 < a * b) :
theorem
mul_le_mul_of_le_of_le
{α : Type u_1}
{a b c d : α}
[mul_zero_class α]
[preorder α]
[pos_mul_mono α]
[mul_pos_mono α]
(h₁ : a ≤ b)
(h₂ : c ≤ d)
(a0 : 0 ≤ a)
(d0 : 0 ≤ d) :
theorem
mul_le_mul
{α : Type u_1}
{a b c d : α}
[mul_zero_class α]
[preorder α]
[pos_mul_mono α]
[mul_pos_mono α]
(h₁ : a ≤ b)
(h₂ : c ≤ d)
(c0 : 0 ≤ c)
(b0 : 0 ≤ b) :
theorem
mul_self_le_mul_self
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[preorder α]
[pos_mul_mono α]
[mul_pos_mono α]
(ha : 0 ≤ a)
(hab : a ≤ b) :
theorem
mul_le_of_mul_le_of_nonneg_left
{α : Type u_1}
{a b c d : α}
[mul_zero_class α]
[preorder α]
[pos_mul_mono α]
(h : a * b ≤ c)
(hle : d ≤ b)
(a0 : 0 ≤ a) :
theorem
le_mul_of_le_mul_of_nonneg_left
{α : Type u_1}
{a b c d : α}
[mul_zero_class α]
[preorder α]
[pos_mul_mono α]
(h : a ≤ b * c)
(hle : c ≤ d)
(b0 : 0 ≤ b) :
theorem
mul_le_of_mul_le_of_nonneg_right
{α : Type u_1}
{a b c d : α}
[mul_zero_class α]
[preorder α]
[mul_pos_mono α]
(h : a * b ≤ c)
(hle : d ≤ a)
(b0 : 0 ≤ b) :
theorem
le_mul_of_le_mul_of_nonneg_right
{α : Type u_1}
{a b c d : α}
[mul_zero_class α]
[preorder α]
[mul_pos_mono α]
(h : a ≤ b * c)
(hle : b ≤ d)
(c0 : 0 ≤ c) :
theorem
pos_mul_mono_iff_covariant_pos
{α : Type u_1}
[mul_zero_class α]
[partial_order α] :
pos_mul_mono α ↔ covariant_class {x // 0 < x} α (λ (x : {x // 0 < x}) (y : α), ↑x * y) has_le.le
theorem
mul_pos_mono_iff_covariant_pos
{α : Type u_1}
[mul_zero_class α]
[partial_order α] :
mul_pos_mono α ↔ covariant_class {x // 0 < x} α (λ (x : {x // 0 < x}) (y : α), y * ↑x) has_le.le
theorem
pos_mul_reflect_lt_iff_contravariant_pos
{α : Type u_1}
[mul_zero_class α]
[partial_order α] :
pos_mul_reflect_lt α ↔ contravariant_class {x // 0 < x} α (λ (x : {x // 0 < x}) (y : α), ↑x * y) has_lt.lt
theorem
mul_pos_reflect_lt_iff_contravariant_pos
{α : Type u_1}
[mul_zero_class α]
[partial_order α] :
mul_pos_reflect_lt α ↔ contravariant_class {x // 0 < x} α (λ (x : {x // 0 < x}) (y : α), y * ↑x) has_lt.lt
@[protected, instance]
def
pos_mul_strict_mono.to_pos_mul_mono
{α : Type u_1}
[mul_zero_class α]
[partial_order α]
[pos_mul_strict_mono α] :
@[protected, instance]
def
mul_pos_strict_mono.to_mul_pos_mono
{α : Type u_1}
[mul_zero_class α]
[partial_order α]
[mul_pos_strict_mono α] :
@[protected, instance]
def
pos_mul_mono_rev.to_pos_mul_reflect_lt
{α : Type u_1}
[mul_zero_class α]
[partial_order α]
[pos_mul_mono_rev α] :
@[protected, instance]
def
mul_pos_mono_rev.to_mul_pos_reflect_lt
{α : Type u_1}
[mul_zero_class α]
[partial_order α]
[mul_pos_mono_rev α] :
theorem
mul_left_cancel_iff_of_pos
{α : Type u_1}
{a b c : α}
[mul_zero_class α]
[partial_order α]
[pos_mul_mono_rev α]
(a0 : 0 < a) :
theorem
mul_right_cancel_iff_of_pos
{α : Type u_1}
{a b c : α}
[mul_zero_class α]
[partial_order α]
[mul_pos_mono_rev α]
(b0 : 0 < b) :
theorem
mul_eq_mul_iff_eq_and_eq_of_pos
{α : Type u_1}
{a b c d : α}
[mul_zero_class α]
[partial_order α]
[pos_mul_strict_mono α]
[mul_pos_strict_mono α]
[pos_mul_mono_rev α]
[mul_pos_mono_rev α]
(hac : a ≤ b)
(hbd : c ≤ d)
(a0 : 0 < a)
(d0 : 0 < d) :
theorem
mul_eq_mul_iff_eq_and_eq_of_pos'
{α : Type u_1}
{a b c d : α}
[mul_zero_class α]
[partial_order α]
[pos_mul_strict_mono α]
[mul_pos_strict_mono α]
[pos_mul_mono_rev α]
[mul_pos_mono_rev α]
(hac : a ≤ b)
(hbd : c ≤ d)
(b0 : 0 < b)
(c0 : 0 < c) :
theorem
pos_and_pos_or_neg_and_neg_of_mul_pos
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[linear_order α]
[pos_mul_mono α]
[mul_pos_mono α]
(hab : 0 < a * b) :
theorem
neg_of_mul_pos_right
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[linear_order α]
[pos_mul_mono α]
[mul_pos_mono α]
(h : 0 < a * b)
(ha : a ≤ 0) :
b < 0
theorem
neg_of_mul_pos_left
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[linear_order α]
[pos_mul_mono α]
[mul_pos_mono α]
(h : 0 < a * b)
(ha : b ≤ 0) :
a < 0
theorem
neg_iff_neg_of_mul_pos
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[linear_order α]
[pos_mul_mono α]
[mul_pos_mono α]
(hab : 0 < a * b) :
theorem
left.neg_of_mul_neg_left
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[linear_order α]
[pos_mul_mono α]
(h : a * b < 0)
(h1 : 0 ≤ a) :
b < 0
theorem
right.neg_of_mul_neg_left
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[linear_order α]
[mul_pos_mono α]
(h : a * b < 0)
(h1 : 0 ≤ a) :
b < 0
theorem
left.neg_of_mul_neg_right
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[linear_order α]
[pos_mul_mono α]
(h : a * b < 0)
(h1 : 0 ≤ b) :
a < 0
theorem
right.neg_of_mul_neg_right
{α : Type u_1}
{a b : α}
[mul_zero_class α]
[linear_order α]
[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
le_mul_iff_one_le_right
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
[pos_mul_mono_rev α]
(a0 : 0 < a) :
@[simp]
theorem
lt_mul_iff_one_lt_right
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
[pos_mul_reflect_lt α]
(a0 : 0 < a) :
@[simp]
theorem
mul_le_iff_le_one_right
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
[pos_mul_mono_rev α]
(a0 : 0 < a) :
@[simp]
theorem
mul_lt_iff_lt_one_right
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
[pos_mul_reflect_lt α]
(a0 : 0 < a) :
Lemmas of the form a ≤ b * a ↔ 1 ≤ b and a * b ≤ b ↔ a ≤ 1,
which assume right covariance.
@[simp]
theorem
le_mul_iff_one_le_left
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
[mul_pos_mono_rev α]
(a0 : 0 < a) :
@[simp]
theorem
lt_mul_iff_one_lt_left
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_strict_mono α]
[mul_pos_reflect_lt α]
(a0 : 0 < a) :
@[simp]
theorem
mul_le_iff_le_one_left
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
[mul_pos_mono_rev α]
(b0 : 0 < b) :
@[simp]
theorem
mul_lt_iff_lt_one_left
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_strict_mono α]
[mul_pos_reflect_lt α]
(b0 : 0 < b) :
Lemmas of the form 1 ≤ b → a ≤ a * b.
Variants with < 0 and ≤ 0 instead of 0 < and 0 ≤ appear in algebra/order/ring/defs (which
imports this file) as they need additional results which are not yet available here.
theorem
mul_le_of_le_one_left
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(hb : 0 ≤ b)
(h : a ≤ 1) :
theorem
le_mul_of_one_le_left
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(hb : 0 ≤ b)
(h : 1 ≤ a) :
theorem
mul_le_of_le_one_right
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(ha : 0 ≤ a)
(h : b ≤ 1) :
theorem
le_mul_of_one_le_right
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(ha : 0 ≤ a)
(h : 1 ≤ b) :
theorem
mul_lt_of_lt_one_left
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_strict_mono α]
(hb : 0 < b)
(h : a < 1) :
theorem
lt_mul_of_one_lt_left
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_strict_mono α]
(hb : 0 < b)
(h : 1 < a) :
theorem
mul_lt_of_lt_one_right
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
(ha : 0 < a)
(h : b < 1) :
theorem
lt_mul_of_one_lt_right
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
(ha : 0 < a)
(h : 1 < b) :
Lemmas of the form b ≤ c → a ≤ 1 → b * a ≤ c.
theorem
mul_le_of_le_of_le_one_of_nonneg
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(h : b ≤ c)
(ha : a ≤ 1)
(hb : 0 ≤ b) :
theorem
mul_lt_of_le_of_lt_one_of_pos
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
(bc : b ≤ c)
(ha : a < 1)
(b0 : 0 < b) :
theorem
mul_lt_of_lt_of_le_one_of_nonneg
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(h : b < c)
(ha : a ≤ 1)
(hb : 0 ≤ b) :
theorem
left.mul_le_one_of_le_of_le
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(ha : a ≤ 1)
(hb : b ≤ 1)
(a0 : 0 ≤ a) :
Assumes left covariance.
theorem
left.mul_lt_of_le_of_lt_one_of_pos
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
(ha : a ≤ 1)
(hb : b < 1)
(a0 : 0 < a) :
Assumes left covariance.
theorem
left.mul_lt_of_lt_of_le_one_of_nonneg
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(ha : a < 1)
(hb : b ≤ 1)
(a0 : 0 ≤ a) :
Assumes left covariance.
theorem
mul_le_of_le_of_le_one'
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
[mul_pos_mono α]
(bc : b ≤ c)
(ha : a ≤ 1)
(a0 : 0 ≤ a)
(c0 : 0 ≤ c) :
theorem
mul_lt_of_lt_of_le_one'
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
[mul_pos_strict_mono α]
(bc : b < c)
(ha : a ≤ 1)
(a0 : 0 < a)
(c0 : 0 ≤ c) :
theorem
mul_lt_of_le_of_lt_one'
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
[mul_pos_mono α]
(bc : b ≤ c)
(ha : a < 1)
(a0 : 0 ≤ a)
(c0 : 0 < c) :
theorem
mul_lt_of_lt_of_lt_one_of_pos
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
[mul_pos_strict_mono α]
(bc : b < c)
(ha : a ≤ 1)
(a0 : 0 < a)
(c0 : 0 ≤ c) :
Lemmas of the form b ≤ c → 1 ≤ a → b ≤ c * a.
theorem
le_mul_of_le_of_one_le_of_nonneg
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(h : b ≤ c)
(ha : 1 ≤ a)
(hc : 0 ≤ c) :
theorem
lt_mul_of_le_of_one_lt_of_pos
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
(bc : b ≤ c)
(ha : 1 < a)
(c0 : 0 < c) :
theorem
lt_mul_of_lt_of_one_le_of_nonneg
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(h : b < c)
(ha : 1 ≤ a)
(hc : 0 ≤ c) :
theorem
left.one_le_mul_of_le_of_le
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(ha : 1 ≤ a)
(hb : 1 ≤ b)
(a0 : 0 ≤ a) :
Assumes left covariance.
theorem
left.one_lt_mul_of_le_of_lt_of_pos
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
(ha : 1 ≤ a)
(hb : 1 < b)
(a0 : 0 < a) :
Assumes left covariance.
theorem
left.lt_mul_of_lt_of_one_le_of_nonneg
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(ha : 1 < a)
(hb : 1 ≤ b)
(a0 : 0 ≤ a) :
Assumes left covariance.
theorem
le_mul_of_le_of_one_le'
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
[mul_pos_mono α]
(bc : b ≤ c)
(ha : 1 ≤ a)
(a0 : 0 ≤ a)
(b0 : 0 ≤ b) :
theorem
lt_mul_of_le_of_one_lt'
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
[mul_pos_mono α]
(bc : b ≤ c)
(ha : 1 < a)
(a0 : 0 ≤ a)
(b0 : 0 < b) :
theorem
lt_mul_of_lt_of_one_le'
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
[mul_pos_strict_mono α]
(bc : b < c)
(ha : 1 ≤ a)
(a0 : 0 < a)
(b0 : 0 ≤ b) :
theorem
lt_mul_of_lt_of_one_lt_of_pos
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
[mul_pos_strict_mono α]
(bc : b < c)
(ha : 1 < a)
(a0 : 0 < a)
(b0 : 0 < b) :
Lemmas of the form a ≤ 1 → b ≤ c → a * b ≤ c.
theorem
mul_le_of_le_one_of_le_of_nonneg
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(ha : a ≤ 1)
(h : b ≤ c)
(hb : 0 ≤ b) :
theorem
mul_lt_of_lt_one_of_le_of_pos
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_strict_mono α]
(ha : a < 1)
(h : b ≤ c)
(hb : 0 < b) :
theorem
mul_lt_of_le_one_of_lt_of_nonneg
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(ha : a ≤ 1)
(h : b < c)
(hb : 0 ≤ b) :
theorem
right.mul_lt_one_of_lt_of_le_of_pos
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_strict_mono α]
(ha : a < 1)
(hb : b ≤ 1)
(b0 : 0 < b) :
Assumes right covariance.
theorem
right.mul_lt_one_of_le_of_lt_of_nonneg
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(ha : a ≤ 1)
(hb : b < 1)
(b0 : 0 ≤ b) :
Assumes right covariance.
theorem
mul_lt_of_lt_one_of_lt_of_pos
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
[mul_pos_strict_mono α]
(ha : a < 1)
(bc : b < c)
(a0 : 0 < a)
(c0 : 0 < c) :
theorem
right.mul_le_one_of_le_of_le
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(ha : a ≤ 1)
(hb : b ≤ 1)
(b0 : 0 ≤ b) :
Assumes right covariance.
theorem
mul_le_of_le_one_of_le'
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
[mul_pos_mono α]
(ha : a ≤ 1)
(bc : b ≤ c)
(a0 : 0 ≤ a)
(c0 : 0 ≤ c) :
theorem
mul_lt_of_lt_one_of_le'
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
[mul_pos_strict_mono α]
(ha : a < 1)
(bc : b ≤ c)
(a0 : 0 ≤ a)
(c0 : 0 < c) :
theorem
mul_lt_of_le_one_of_lt'
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_strict_mono α]
[mul_pos_mono α]
(ha : a ≤ 1)
(bc : b < c)
(a0 : 0 < a)
(c0 : 0 ≤ c) :
Lemmas of the form 1 ≤ a → b ≤ c → b ≤ a * c.
theorem
lt_mul_of_one_lt_of_le_of_pos
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_strict_mono α]
(ha : 1 < a)
(h : b ≤ c)
(hc : 0 < c) :
theorem
lt_mul_of_one_le_of_lt_of_nonneg
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(ha : 1 ≤ a)
(h : b < c)
(hc : 0 ≤ c) :
theorem
lt_mul_of_one_lt_of_lt_of_pos
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_strict_mono α]
(ha : 1 < a)
(h : b < c)
(hc : 0 < c) :
theorem
right.one_lt_mul_of_lt_of_le_of_pos
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_strict_mono α]
(ha : 1 < a)
(hb : 1 ≤ b)
(b0 : 0 < b) :
Assumes right covariance.
theorem
right.one_lt_mul_of_le_of_lt_of_nonneg
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(ha : 1 ≤ a)
(hb : 1 < b)
(b0 : 0 ≤ b) :
Assumes right covariance.
theorem
right.one_lt_mul_of_lt_of_lt
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_strict_mono α]
(ha : 1 < a)
(hb : 1 < b)
(b0 : 0 < b) :
Assumes right covariance.
theorem
lt_mul_of_one_lt_of_lt_of_nonneg
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(ha : 1 ≤ a)
(h : b < c)
(hc : 0 ≤ c) :
theorem
lt_of_mul_lt_of_one_le_of_nonneg_left
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(h : a * b < c)
(hle : 1 ≤ b)
(ha : 0 ≤ a) :
a < c
theorem
lt_of_lt_mul_of_le_one_of_nonneg_left
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(h : a < b * c)
(hc : c ≤ 1)
(hb : 0 ≤ b) :
a < b
theorem
lt_of_lt_mul_of_le_one_of_nonneg_right
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(h : a < b * c)
(hb : b ≤ 1)
(hc : 0 ≤ c) :
a < c
theorem
le_mul_of_one_le_of_le_of_nonneg
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(ha : 1 ≤ a)
(bc : b ≤ c)
(c0 : 0 ≤ c) :
theorem
right.one_le_mul_of_le_of_le
{α : Type u_1}
{a b : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(ha : 1 ≤ a)
(hb : 1 ≤ b)
(b0 : 0 ≤ b) :
Assumes right covariance.
theorem
le_of_mul_le_of_one_le_of_nonneg_left
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(h : a * b ≤ c)
(hb : 1 ≤ b)
(ha : 0 ≤ a) :
a ≤ c
theorem
le_of_le_mul_of_le_one_of_nonneg_left
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[pos_mul_mono α]
(h : a ≤ b * c)
(hc : c ≤ 1)
(hb : 0 ≤ b) :
a ≤ b
theorem
le_of_mul_le_of_one_le_nonneg_right
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(h : a * b ≤ c)
(ha : 1 ≤ a)
(hb : 0 ≤ b) :
b ≤ c
theorem
le_of_le_mul_of_le_one_of_nonneg_right
{α : Type u_1}
{a b c : α}
[mul_one_class α]
[has_zero α]
[preorder α]
[mul_pos_mono α]
(h : a ≤ b * c)
(hb : b ≤ 1)
(hc : 0 ≤ c) :
a ≤ c
theorem
exists_square_le'
{α : Type u_1}
{a : α}
[mul_one_class α]
[has_zero α]
[linear_order α]
[pos_mul_strict_mono α]
(a0 : 0 < a) :
theorem
pos_mul_mono.to_pos_mul_strict_mono
{α : Type u_1}
[cancel_monoid_with_zero α]
[partial_order α]
[pos_mul_mono α] :
theorem
pos_mul_mono_iff_pos_mul_strict_mono
{α : Type u_1}
[cancel_monoid_with_zero α]
[partial_order α] :
theorem
mul_pos_mono.to_mul_pos_strict_mono
{α : Type u_1}
[cancel_monoid_with_zero α]
[partial_order α]
[mul_pos_mono α] :
theorem
mul_pos_mono_iff_mul_pos_strict_mono
{α : Type u_1}
[cancel_monoid_with_zero α]
[partial_order α] :
theorem
pos_mul_reflect_lt.to_pos_mul_mono_rev
{α : Type u_1}
[cancel_monoid_with_zero α]
[partial_order α]
[pos_mul_reflect_lt α] :
theorem
pos_mul_mono_rev_iff_pos_mul_reflect_lt
{α : Type u_1}
[cancel_monoid_with_zero α]
[partial_order α] :
theorem
mul_pos_reflect_lt.to_mul_pos_mono_rev
{α : Type u_1}
[cancel_monoid_with_zero α]
[partial_order α]
[mul_pos_reflect_lt α] :
theorem
mul_pos_mono_rev_iff_mul_pos_reflect_lt
{α : Type u_1}
[cancel_monoid_with_zero α]
[partial_order α] :
theorem
pos_mul_strict_mono_iff_mul_pos_strict_mono
{α : Type u_1}
[comm_semigroup α]
[has_zero α]
[preorder α] :
theorem
pos_mul_reflect_lt_iff_mul_pos_reflect_lt
{α : Type u_1}
[comm_semigroup α]
[has_zero α]
[preorder α] :
theorem
pos_mul_mono_rev_iff_mul_pos_mono_rev
{α : Type u_1}
[comm_semigroup α]
[has_zero α]
[preorder α] :