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) (≤), abbreviated pos_mul_mono α, expressing that multiplication by positive elements on the left is monotone;
• • covariant_class α>0 α (λ x y, x * y) (<), abbreviated pos_mul_strict_mono α, expressing that multiplication by positive elements on the left is strictly monotone;
• monotone right
• • covariant_class α>0 α (λ x y, y * x) (≤), abbreviated mul_pos_mono α, expressing that multiplication by positive elements on the right is monotone;
• • covariant_class α>0 α (λ x y, y * x) (<), abbreviated mul_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) (≤), abbreviated pos_mul_mono_rev α, expressing that multiplication by positive elements on the left is reverse monotone;
• • contravariant_class α>0 α (λ x y, x * y) (<), abbreviated pos_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) (≤), abbreviated mul_pos_mono_rev α, expressing that multiplication by positive elements on the right is reverse monotone;
• • contravariant_class α>0 α (λ x y, y * x) (<), abbreviated mul_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}

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

Lemmas of the form b ≤ c → 1 ≤ a → b ≤ c * a.

Lemmas of the form a ≤ 1 → b ≤ c → a * b ≤ c.

Lemmas of the form 1 ≤ a → b ≤ c → b ≤ a * c.