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
)
CovariantClass
es to assume that multiplication by positive elements is (strictly) monotone on a
MulZeroClass
, MonoidWithZero
,...
More specifically, we use extensively the following typeclasses:
- monotone left
-
CovariantClass α>0 α (fun x y ↦ x * y) (≤)
, abbreviatedPosMulMono α
, expressing that multiplication by positive elements on the left is monotone;
-
CovariantClass α>0 α (fun x y ↦ x * y) (<)
, abbreviatedPosMulStrictMono α
, expressing that multiplication by positive elements on the left is strictly monotone;
- monotone right
-
CovariantClass α>0 α (fun x y ↦ y * x) (≤)
, abbreviatedMulPosMono α
, expressing that multiplication by positive elements on the right is monotone;
-
CovariantClass α>0 α (fun x y ↦ y * x) (<)
, abbreviatedMulPosStrictMono α
, expressing that multiplication by positive elements on the right is strictly monotone.
- reverse monotone left
-
ContravariantClass α>0 α (fun x y ↦ x * y) (≤)
, abbreviatedPosMulMonoRev α
, expressing that multiplication by positive elements on the left is reverse monotone;
-
ContravariantClass α>0 α (fun x y ↦ x * y) (<)
, abbreviatedPosMulReflectLT α
, expressing that multiplication by positive elements on the left is strictly reverse monotone;
- reverse reverse monotone right
-
ContravariantClass α>0 α (fun x y ↦ y * x) (≤)
, abbreviatedMulPosMonoRev α
, expressing that multiplication by positive elements on the right is reverse monotone;
-
ContravariantClass α>0 α (fun x y ↦ y * x) (<)
, abbreviatedMulPosReflectLT α
, 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}
Local notation for the nonnegative elements of a type α
. TODO: actually make local.
Instances For
Local notation for the positive elements of a type α
. TODO: actually make local.
Instances For
PosMulMono α
is an abbreviation for CovariantClass α≥0 α (fun x y ↦ x * y) (≤)
,
expressing that multiplication by nonnegative elements on the left is monotone.
Instances For
MulPosMono α
is an abbreviation for CovariantClass α≥0 α (fun x y ↦ y * x) (≤)
,
expressing that multiplication by nonnegative elements on the right is monotone.
Instances For
PosMulStrictMono α
is an abbreviation for CovariantClass α>0 α (fun x y ↦ x * y) (<)
,
expressing that multiplication by positive elements on the left is strictly monotone.
Instances For
MulPosStrictMono α
is an abbreviation for CovariantClass α>0 α (fun x y ↦ y * x) (<)
,
expressing that multiplication by positive elements on the right is strictly monotone.
Instances For
PosMulReflectLT α
is an abbreviation for ContravariantClas α≥0 α (fun x y ↦ x * y) (<)
,
expressing that multiplication by nonnegative elements on the left is strictly reverse monotone.
Instances For
MulPosReflectLT α
is an abbreviation for ContravariantClas α≥0 α (fun x y ↦ y * x) (<)
,
expressing that multiplication by nonnegative elements on the right is strictly reverse monotone.
Instances For
PosMulMonoRev α
is an abbreviation for ContravariantClas α>0 α (fun x y ↦ x * y) (≤)
,
expressing that multiplication by positive elements on the left is reverse monotone.
Instances For
MulPosMonoRev α
is an abbreviation for ContravariantClas α>0 α (fun x y ↦ y * x) (≤)
,
expressing that multiplication by positive elements on the right is reverse monotone.
Instances For
Alias of lt_of_mul_lt_mul_left
.
Alias of lt_of_mul_lt_mul_right
.
Alias of le_of_mul_le_mul_left
.
Alias of le_of_mul_le_mul_right
.
Assumes left covariance.
Alias of Left.mul_pos
.
Assumes left covariance.
Assumes right covariance.
Assumes left covariance.
Alias of Left.mul_nonneg
.
Assumes left covariance.
Assumes right covariance.
Lemmas of the form a ≤ a * b ↔ 1 ≤ b
and a * b ≤ a ↔ b ≤ 1
,
which assume left covariance.
Lemmas of the form a ≤ b * a ↔ 1 ≤ b
and a * b ≤ b ↔ a ≤ 1
,
which assume right covariance.
Lemmas of the form 1 ≤ b → a ≤ a * b
.
Variants with < 0
and ≤ 0
instead of 0 <
and 0 ≤
appear in Mathlib/Algebra/Order/Ring/Defs
(which imports this file) as they need additional results which are not yet available here.
Lemmas of the form b ≤ c → a ≤ 1 → b * a ≤ c
.
Assumes left covariance.
Assumes left covariance.
Assumes left covariance.
Lemmas of the form b ≤ c → 1 ≤ a → b ≤ c * a
.
Assumes left covariance.
Assumes left covariance.
Assumes left covariance.
Lemmas of the form a ≤ 1 → b ≤ c → a * b ≤ c
.
Assumes right covariance.
Assumes right covariance.
Assumes right covariance.
Lemmas of the form 1 ≤ a → b ≤ c → b ≤ a * c
.
Assumes right covariance.
Assumes right covariance.
Assumes right covariance.
Assumes right covariance.