Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs

Module docstring

{"# (Strict) monotonicity of multiplication by nonnegative (positive) elements

This file defines eight typeclasses expressing monotonicity (strict monotonicity) of multiplication on the left or right by nonnegative (positive) elements in a preorder.

For left multiplication (a ↦ b * a) we define the following typeclasses: * PosMulMono: If b ≥ 0, then a₁ ≤ a₂ → b * a₁ ≤ b * a₂. * PosMulStrictMono: If b > 0, then a₁ < a₂ → b * a₁ 0, then b * a₁ ≤ b * a₂ → a₁ ≤ a₂.

For right multiplication (a ↦ a * b) we define the following typeclasses: * MulPosMono: If b ≥ 0, then a₁ ≤ a₂ → a₁ * b ≤ a₂ * b. * MulPosStrictMono: If b > 0, then a₁ < a₂ → a₁ * b < a₂ * b. * MulPosReflectLT: If b ≥ 0, then a₁ * b < a₂ * b → a₁ < a₂. * MulPosReflectLE: If b > 0, then a₁ * b ≤ a₂ * b → a₁ ≤ a₂.

We then provide statements and instances about these typeclasses not requiring MulZeroClass or higher on the underlying type – those that do can be found in Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic.

Less granular typeclasses like OrderedAddCommMonoid and LinearOrderedField should be enough for most purposes, and the system is set up so that they imply the correct granular typeclasses here.

Implications

As the underlying type α gets more structured, some of the above typeclasses become equivalent. The commonly used implications are: * When α is a partial order (in Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic): * PosMulStrictMono.toPosMulMono * MulPosStrictMono.toMulPosMono * PosMulReflectLE.toPosMulReflectLT * MulPosReflectLE.toMulPosReflectLT * When α is a linear order: * PosMulStrictMono.toPosMulReflectLE * MulPosStrictMono.toMulPosReflectLE * When multiplication on α is commutative: * posMulMono_iff_mulPosMono * posMulStrictMono_iff_mulPosStrictMono * posMulReflectLE_iff_mulPosReflectLE * posMulReflectLT_iff_mulPosReflectLT

Furthermore, the bundled non-granular typeclasses imply the granular ones like so: * OrderedSemiring → PosMulMono * OrderedSemiring → MulPosMono * StrictOrderedSemiring → PosMulStrictMono * StrictOrderedSemiring → MulPosStrictMono

All these are registered as instances, which means that in practice you should not worry about these implications. However, if you encounter a case where you think a statement is true but not covered by the current implications, please bring it up on Zulip!

Notation

The following is local notation in this file: * α≥0: {x : α // 0 ≤ x} * α>0: {x : α // 0 < x}

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/notation.20for.20positive.20elements for a discussion about this notation, and whether to enable it globally (note that the notation is currently global but broken, hence actually only works locally). "}

PosMulMono structure

extends CovariantClass α≥0 α (fun x y => x * y) (· ≤ ·)

Full source

/-- Typeclass for monotonicity of multiplication by nonnegative elements on the left,
namely `a₁ ≤ a₂ → b * a₁ ≤ b * a₂` if `0 ≤ b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedSemiring`. -/
@[mk_iff] class PosMulMono : Prop extends CovariantClass α≥0 α (fun x y => x * y) (· ≤ ·)

Monotonicity of left multiplication by nonnegative elements

Informal description

A typeclass expressing that left multiplication by nonnegative elements is monotone, i.e., for any $b \geq 0$ and any $a_1 \leq a_2$, we have $b \cdot a_1 \leq b \cdot a_2$. This is a granular typeclass typically used to derive more general ordered algebraic structures like `OrderedSemiring`.

PosMulStrictMono structure

extends CovariantClass α>0 α (fun x y => x * y) (· < ·)

Full source

/-- Typeclass for strict monotonicity of multiplication by positive elements on the left,
namely `a₁ < a₂ → b * a₁ < b * a₂` if `0 < b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`StrictOrderedSemiring`. -/
@[mk_iff] class PosMulStrictMono : Prop extends CovariantClass α>0 α (fun x y => x * y) (· < ·)

Strict monotonicity of left multiplication by positive elements

Informal description

The structure `PosMulStrictMono` represents the property that left multiplication by positive elements is strictly monotone. Specifically, for any positive element $ b > 0 $ in a preorder $ \alpha $, if $ a_1 < a_2 $, then $ b \cdot a_1 < b \cdot a_2 $.

PosMulReflectLT structure

extends ContravariantClass α≥0 α (fun x y => x * y) (· < ·)

Full source

/-- Typeclass for strict reverse monotonicity of multiplication by nonnegative elements on
the left, namely `b * a₁ < b * a₂ → a₁ < a₂` if `0 ≤ b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`LinearOrderedSemiring`. -/
@[mk_iff] class PosMulReflectLT : Prop extends ContravariantClass α≥0 α (fun x y => x * y) (· < ·)

Strict order reflection by left multiplication with nonnegative elements

Informal description

A structure representing the property that for any nonnegative element $b$ in a preorder $\alpha$, left multiplication by $b$ reflects the strict order: if $b \cdot a_1 < b \cdot a_2$, then $a_1 < a_2$.

PosMulReflectLE structure

extends ContravariantClass α>0 α (fun x y => x * y) (· ≤ ·)

Full source

/-- Typeclass for reverse monotonicity of multiplication by positive elements on the left,
namely `b * a₁ ≤ b * a₂ → a₁ ≤ a₂` if `0 < b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`LinearOrderedSemiring`. -/
@[mk_iff] class PosMulReflectLE : Prop extends ContravariantClass α>0 α (fun x y => x * y) (· ≤ ·)

Reverse monotonicity of left multiplication by positive elements

Informal description

A structure representing the property that for any positive element $ b $ in a type $ \alpha $, if $ b \cdot a_1 \leq b \cdot a_2 $, then $ a_1 \leq a_2 $. This captures the reverse monotonicity of left multiplication by positive elements with respect to the order relation $ \leq $.

MulPosMono structure

extends CovariantClass α≥0 α (fun x y => y * x) (· ≤ ·)

Full source

/-- Typeclass for monotonicity of multiplication by nonnegative elements on the right,
namely `a₁ ≤ a₂ → a₁ * b ≤ a₂ * b` if `0 ≤ b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedSemiring`. -/
@[mk_iff] class MulPosMono : Prop extends CovariantClass α≥0 α (fun x y => y * x) (· ≤ ·)

Monotonicity of right multiplication by nonnegative elements

Informal description

The structure `MulPosMono` represents the property that right multiplication by nonnegative elements is monotone. That is, for any nonnegative element $b$ in a preorder $\alpha$, if $a_1 \leq a_2$, then $a_1 * b \leq a_2 * b$.

MulPosStrictMono structure

extends CovariantClass α>0 α (fun x y => y * x) (· < ·)

Full source

/-- Typeclass for strict monotonicity of multiplication by positive elements on the right,
namely `a₁ < a₂ → a₁ * b < a₂ * b` if `0 < b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`StrictOrderedSemiring`. -/
@[mk_iff] class MulPosStrictMono : Prop extends CovariantClass α>0 α (fun x y => y * x) (· < ·)

Strict monotonicity of right multiplication by positive elements

Informal description

The structure `MulPosStrictMono` represents the property that right multiplication by a positive element is strictly monotone. That is, for any positive element $ b > 0 $ in a preorder $ \alpha $, if $ a_1 < a_2 $, then $ a_1 * b < a_2 * b $.

MulPosReflectLT structure

extends ContravariantClass α≥0 α (fun x y => y * x) (· < ·)

Full source

/-- Typeclass for strict reverse monotonicity of multiplication by nonnegative elements on
the right, namely `a₁ * b < a₂ * b → a₁ < a₂` if `0 ≤ b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`LinearOrderedSemiring`. -/
@[mk_iff] class MulPosReflectLT : Prop extends ContravariantClass α≥0 α (fun x y => y * x) (· < ·)

Reflection of strict order under right multiplication by nonnegative elements

Informal description

The structure `MulPosReflectLT` represents the property that for any nonnegative element $b$ in a preorder $\alpha$, right multiplication by $b$ reflects the strict order relation. That is, if $a_1 * b < a_2 * b$ for some $a_1, a_2 \in \alpha$, then $a_1 < a_2$.

MulPosReflectLE structure

extends ContravariantClass α>0 α (fun x y => y * x) (· ≤ ·)

Full source

/-- Typeclass for reverse monotonicity of multiplication by positive elements on the right,
namely `a₁ * b ≤ a₂ * b → a₁ ≤ a₂` if `0 < b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`LinearOrderedSemiring`. -/
@[mk_iff] class MulPosReflectLE : Prop extends ContravariantClass α>0 α (fun x y => y * x) (· ≤ ·)

Reflection of non-strict order under right multiplication by positive elements

Informal description

The structure `MulPosReflectLE` represents the property that for any positive element $ b > 0 $ in a preorder $ \alpha $, right multiplication by $ b $ reflects the non-strict order relation. That is, if $ a_1 * b \leq a_2 * b $ for some $ a_1, a_2 \in \alpha $, then $ a_1 \leq a_2 $.

PosMulMono.to_covariantClass_pos_mul_le instance

[PosMulMono α] : CovariantClass α>0 α (fun x y => x * y) (· ≤ ·)

Full source

instance PosMulMono.to_covariantClass_pos_mul_le [PosMulMono α] :
    CovariantClass α>0 α (fun x y => x * y) (· ≤ ·) :=
  ⟨fun a _ _ bc => @CovariantClass.elim α≥0 α (fun x y => x * y) (· ≤ ·) _ ⟨_, a.2.le⟩ _ _ bc⟩

Monotonicity of Left Multiplication by Positive Elements in Preorders

Informal description

For any preorder $\alpha$ where left multiplication by nonnegative elements is monotone (i.e., $b \geq 0$ and $a_1 \leq a_2$ implies $b \cdot a_1 \leq b \cdot a_2$), left multiplication by positive elements is also monotone. That is, for any $b > 0$ and $a_1 \leq a_2$, we have $b \cdot a_1 \leq b \cdot a_2$.

MulPosMono.to_covariantClass_pos_mul_le instance

[MulPosMono α] : CovariantClass α>0 α (fun x y => y * x) (· ≤ ·)

Full source

instance MulPosMono.to_covariantClass_pos_mul_le [MulPosMono α] :
    CovariantClass α>0 α (fun x y => y * x) (· ≤ ·) :=
  ⟨fun a _ _ bc => @CovariantClass.elim α≥0 α (fun x y => y * x) (· ≤ ·) _ ⟨_, a.2.le⟩ _ _ bc⟩

Monotonicity of Right Multiplication by Positive Elements in Preorders

Informal description

For any preorder $\alpha$ where right multiplication by nonnegative elements is monotone (i.e., $b \geq 0$ and $a_1 \leq a_2$ implies $a_1 \cdot b \leq a_2 \cdot b$), right multiplication by positive elements is also monotone. That is, for any $b > 0$ and $a_1 \leq a_2$, we have $a_1 \cdot b \leq a_2 \cdot b$.

PosMulReflectLT.to_contravariantClass_pos_mul_lt instance

[PosMulReflectLT α] : ContravariantClass α>0 α (fun x y => x * y) (· < ·)

Full source

instance PosMulReflectLT.to_contravariantClass_pos_mul_lt [PosMulReflectLT α] :
    ContravariantClass α>0 α (fun x y => x * y) (· < ·) :=
  ⟨fun a _ _ bc => @ContravariantClass.elim α≥0 α (fun x y => x * y) (· < ·) _ ⟨_, a.2.le⟩ _ _ bc⟩

Strict Order Reflection by Left Multiplication with Positive Elements

Informal description

For any preorder $\alpha$ where left multiplication by nonnegative elements reflects the strict order (i.e., if $b \geq 0$ and $b \cdot a_1 0$ and $b \cdot a_1 < b \cdot a_2$, we have $a_1 < a_2$.

MulPosReflectLT.to_contravariantClass_pos_mul_lt instance

[MulPosReflectLT α] : ContravariantClass α>0 α (fun x y => y * x) (· < ·)

Full source

instance MulPosReflectLT.to_contravariantClass_pos_mul_lt [MulPosReflectLT α] :
    ContravariantClass α>0 α (fun x y => y * x) (· < ·) :=
  ⟨fun a _ _ bc => @ContravariantClass.elim α≥0 α (fun x y => y * x) (· < ·) _ ⟨_, a.2.le⟩ _ _ bc⟩

Strict Order Reflection by Right Multiplication with Positive Elements

Informal description

For any preorder $\alpha$ where right multiplication by nonnegative elements reflects the strict order (i.e., if $b \geq 0$ and $a_1 * b < a_2 * b$, then $a_1 < a_2$), right multiplication by positive elements also reflects the strict order. That is, for any $b > 0$ and $a_1 * b < a_2 * b$, we have $a_1 < a_2$.

MulLeftMono.toPosMulMono instance

[MulLeftMono α] : PosMulMono α

Full source

instance (priority := 100) MulLeftMono.toPosMulMono [MulLeftMono α] :
    PosMulMono α where elim _ _ := ‹MulLeftMono α›.elim _

Monotonicity of Left Multiplication Implies Monotonicity by Nonnegative Elements

Informal description

For any preorder $\alpha$ where left multiplication is monotone (i.e., $a_1 \leq a_2$ implies $b \cdot a_1 \leq b \cdot a_2$ for all $b \in \alpha$), left multiplication by nonnegative elements is also monotone.

MulRightMono.toMulPosMono instance

[MulRightMono α] : MulPosMono α

Full source

instance (priority := 100) MulRightMono.toMulPosMono [MulRightMono α] :
    MulPosMono α where elim _ _ := ‹MulRightMono α›.elim _

Monotonicity of Right Multiplication Implies Monotonicity by Nonnegative Elements

Informal description

For any preorder $\alpha$ where right multiplication is monotone (i.e., $a_1 \leq a_2$ implies $a_1 \cdot b \leq a_2 \cdot b$ for all $b \in \alpha$), right multiplication by nonnegative elements is also monotone.

MulLeftStrictMono.toPosMulStrictMono instance

[MulLeftStrictMono α] : PosMulStrictMono α

Full source

instance (priority := 100) MulLeftStrictMono.toPosMulStrictMono [MulLeftStrictMono α] :
    PosMulStrictMono α where elim _ _ := ‹MulLeftStrictMono α›.elim _

Strict Monotonicity of Left Multiplication Implies Strict Monotonicity by Positive Elements

Informal description

For any preorder $\alpha$ where left multiplication is strictly monotone (i.e., $a_1 < a_2$ implies $b \cdot a_1 < b \cdot a_2$ for all $b \in \alpha$), left multiplication by positive elements is also strictly monotone.

MulRightStrictMono.toMulPosStrictMono instance

[MulRightStrictMono α] : MulPosStrictMono α

Full source

instance (priority := 100) MulRightStrictMono.toMulPosStrictMono [MulRightStrictMono α] :
    MulPosStrictMono α where elim _ _ := ‹MulRightStrictMono α›.elim _

Strict Monotonicity of Right Multiplication Implies Strict Monotonicity by Positive Elements

Informal description

For any preorder $\alpha$ where right multiplication is strictly monotone (i.e., $a_1 < a_2$ implies $a_1 \cdot b < a_2 \cdot b$ for all $b \in \alpha$), right multiplication by positive elements is also strictly monotone.

MulLeftMono.toPosMulReflectLT instance

[MulLeftReflectLT α] : PosMulReflectLT α

Full source

instance (priority := 100) MulLeftMono.toPosMulReflectLT [MulLeftReflectLT α] :
   PosMulReflectLT α where elim _ _ := ‹MulLeftReflectLT α›.elim _

Strict Order Reflection by Left Multiplication with Nonnegative Elements

Informal description

For any preorder $\alpha$ where left multiplication reflects the strict order (i.e., $b \cdot a_1 < b \cdot a_2$ implies $a_1 < a_2$ for all $b \in \alpha$), left multiplication by nonnegative elements also reflects the strict order.

MulRightMono.toMulPosReflectLT instance

[MulRightReflectLT α] : MulPosReflectLT α

Full source

instance (priority := 100) MulRightMono.toMulPosReflectLT [MulRightReflectLT α] :
   MulPosReflectLT α where elim _ _ := ‹MulRightReflectLT α›.elim _

Reflection of Strict Order under Right Multiplication by Nonnegative Elements

Informal description

For any preorder $\alpha$ where right multiplication reflects the strict order (i.e., $a_1 * b < a_2 * b$ implies $a_1 < a_2$ for all $b \in \alpha$), right multiplication by nonnegative elements also reflects the strict order.

MulLeftStrictMono.toPosMulReflectLE instance

[MulLeftReflectLE α] : PosMulReflectLE α

Full source

instance (priority := 100) MulLeftStrictMono.toPosMulReflectLE [MulLeftReflectLE α] :
   PosMulReflectLE α where elim _ _ := ‹MulLeftReflectLE α›.elim _

Reflection of Non-Strict Order under Left Multiplication by Positive Elements

Informal description

For any preorder $\alpha$ where left multiplication by positive elements reflects the non-strict order relation (i.e., $b \cdot a_1 \leq b \cdot a_2$ implies $a_1 \leq a_2$ for $b > 0$), the structure `PosMulReflectLE` holds.

MulRightStrictMono.toMulPosReflectLE instance

[MulRightReflectLE α] : MulPosReflectLE α

Full source

instance (priority := 100) MulRightStrictMono.toMulPosReflectLE [MulRightReflectLE α] :
   MulPosReflectLE α where elim _ _ := ‹MulRightReflectLE α›.elim _

Reflection of Non-Strict Order under Right Multiplication by Positive Elements

Informal description

For any preorder $\alpha$ where right multiplication by positive elements reflects the non-strict order relation (i.e., $a_1 * b \leq a_2 * b$ implies $a_1 \leq a_2$ for $b > 0$), the structure `MulPosReflectLE` holds.

mul_le_mul_of_nonneg_left theorem

[PosMulMono α] (h : b ≤ c) (a0 : 0 ≤ a) : a * b ≤ a * c

Full source

@[gcongr]
theorem mul_le_mul_of_nonneg_left [PosMulMono α] (h : b ≤ c) (a0 : 0 ≤ a) : a * b ≤ a * c :=
  @CovariantClass.elim α≥0 α (fun x y => x * y) (· ≤ ·) _ ⟨a, a0⟩ _ _ h

Monotonicity of Left Multiplication by Nonnegative Elements: $a \geq 0 \implies (b \leq c \to a \cdot b \leq a \cdot c)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by nonnegative elements is monotone (i.e., the typeclass `PosMulMono α` holds), then for any elements $b, c \in \alpha$ with $b \leq c$ and any nonnegative element $a \geq 0$, we have $a \cdot b \leq a \cdot c$.

mul_le_mul_of_nonneg_right theorem

[MulPosMono α] (h : b ≤ c) (a0 : 0 ≤ a) : b * a ≤ c * a

Full source

@[gcongr]
theorem mul_le_mul_of_nonneg_right [MulPosMono α] (h : b ≤ c) (a0 : 0 ≤ a) : b * a ≤ c * a :=
  @CovariantClass.elim α≥0 α (fun x y => y * x) (· ≤ ·) _ ⟨a, a0⟩ _ _ h

Monotonicity of Right Multiplication by Nonnegative Elements: $a \geq 0 \implies (b \leq c \to b \cdot a \leq c \cdot a)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If right multiplication by nonnegative elements is monotone (i.e., the typeclass `MulPosMono α` holds), then for any elements $b, c \in \alpha$ with $b \leq c$ and any nonnegative element $a \geq 0$, we have $b \cdot a \leq c \cdot a$.

mul_lt_mul_of_pos_left theorem

[PosMulStrictMono α] (bc : b < c) (a0 : 0 < a) : a * b < a * c

Full source

@[gcongr]
theorem mul_lt_mul_of_pos_left [PosMulStrictMono α] (bc : b < c) (a0 : 0 < a) : a * b < a * c :=
  @CovariantClass.elim α>0 α (fun x y => x * y) (· < ·) _ ⟨a, a0⟩ _ _ bc

Strict Monotonicity of Left Multiplication by Positive Elements: $a > 0 \implies (b < c \to a \cdot b < a \cdot c)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by positive elements is strictly monotone (i.e., the typeclass `PosMulStrictMono α` holds), then for any elements $b, c \in \alpha$ with $b < c$ and any positive element $a > 0$, we have $a \cdot b < a \cdot c$.

mul_lt_mul_of_pos_right theorem

[MulPosStrictMono α] (bc : b < c) (a0 : 0 < a) : b * a < c * a

Full source

@[gcongr]
theorem mul_lt_mul_of_pos_right [MulPosStrictMono α] (bc : b < c) (a0 : 0 < a) : b * a < c * a :=
  @CovariantClass.elim α>0 α (fun x y => y * x) (· < ·) _ ⟨a, a0⟩ _ _ bc

Strict Monotonicity of Right Multiplication by Positive Elements: $a > 0 \implies (b < c \to b \cdot a < c \cdot a)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If right multiplication by positive elements is strictly monotone (i.e., the typeclass `MulPosStrictMono α` holds), then for any elements $b, c \in \alpha$ with $b < c$ and any positive element $a > 0$, we have $b \cdot a < c \cdot a$.

lt_of_mul_lt_mul_left theorem

[PosMulReflectLT α] (h : a * b < a * c) (a0 : 0 ≤ a) : b < c

Full source

theorem lt_of_mul_lt_mul_left [PosMulReflectLT α] (h : a * b < a * c) (a0 : 0 ≤ a) : b < c :=
  @ContravariantClass.elim α≥0 α (fun x y => x * y) (· < ·) _ ⟨a, a0⟩ _ _ h

Strict order reflection by left multiplication with nonnegative elements: $a \geq 0 \implies (a \cdot b < a \cdot c \to b < c)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by nonnegative elements reflects the strict order (i.e., the typeclass `PosMulReflectLT α` holds), then for any elements $b, c \in \alpha$ and any nonnegative element $a \geq 0$, the inequality $a \cdot b < a \cdot c$ implies $b < c$.

lt_of_mul_lt_mul_right theorem

[MulPosReflectLT α] (h : b * a < c * a) (a0 : 0 ≤ a) : b < c

Full source

theorem lt_of_mul_lt_mul_right [MulPosReflectLT α] (h : b * a < c * a) (a0 : 0 ≤ a) : b < c :=
  @ContravariantClass.elim α≥0 α (fun x y => y * x) (· < ·) _ ⟨a, a0⟩ _ _ h

Strict order reflection under right multiplication by nonnegative elements: $a \geq 0 \implies (b \cdot a < c \cdot a \to b < c)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If right multiplication by nonnegative elements reflects the strict order (i.e., the typeclass `MulPosReflectLT α` holds), then for any elements $b, c \in \alpha$ and any nonnegative element $a \geq 0$, the inequality $b \cdot a < c \cdot a$ implies $b < c$.

le_of_mul_le_mul_left theorem

[PosMulReflectLE α] (bc : a * b ≤ a * c) (a0 : 0 < a) : b ≤ c

Full source

theorem le_of_mul_le_mul_left [PosMulReflectLE α] (bc : a * b ≤ a * c) (a0 : 0 < a) : b ≤ c :=
  @ContravariantClass.elim α>0 α (fun x y => x * y) (· ≤ ·) _ ⟨a, a0⟩ _ _ bc

Non-strict order reflection under left multiplication by positive elements

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by positive elements reflects the non-strict order (i.e., the typeclass `PosMulReflectLE α` holds), then for any elements $b, c \in \alpha$ and any positive element $a > 0$, the inequality $a \cdot b \leq a \cdot c$ implies $b \leq c$.

le_of_mul_le_mul_right theorem

[MulPosReflectLE α] (bc : b * a ≤ c * a) (a0 : 0 < a) : b ≤ c

Full source

theorem le_of_mul_le_mul_right [MulPosReflectLE α] (bc : b * a ≤ c * a) (a0 : 0 < a) : b ≤ c :=
  @ContravariantClass.elim α>0 α (fun x y => y * x) (· ≤ ·) _ ⟨a, a0⟩ _ _ bc

Non-strict order reflection under right multiplication by positive elements

Informal description

Let $\alpha$ be a preorder with a multiplication operation and a zero element. If right multiplication by positive elements reflects the non-strict order (i.e., $\alpha$ satisfies `MulPosReflectLE`), then for any elements $b, c \in \alpha$ and any positive element $a > 0$, the inequality $b \cdot a \leq c \cdot a$ implies $b \leq c$.

mul_lt_mul_left theorem

[PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) : a * b < a * c ↔ b < c

Full source

@[simp]
theorem mul_lt_mul_left [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) :
    a * b < a * c ↔ b < c :=
  @rel_iff_cov α>0 α (fun x y => x * y) (· < ·) _ _ ⟨a, a0⟩ _ _

Strict Order Preservation and Reflection under Left Multiplication by Positive Elements: $a > 0 \implies (a \cdot b < a \cdot c \leftrightarrow b < c)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by positive elements is strictly monotone (`PosMulStrictMono α`) and left multiplication by nonnegative elements reflects the strict order (`PosMulReflectLT α`), then for any positive element $a > 0$ and any elements $b, c \in \alpha$, we have the equivalence: \[ a \cdot b < a \cdot c \quad \text{if and only if} \quad b < c. \]

mul_lt_mul_right theorem

[MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) : b * a < c * a ↔ b < c

Full source

@[simp]
theorem mul_lt_mul_right [MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) :
    b * a < c * a ↔ b < c :=
  @rel_iff_cov α>0 α (fun x y => y * x) (· < ·) _ _ ⟨a, a0⟩ _ _

Strict Order Preservation and Reflection under Right Multiplication by Positive Elements: $a > 0 \implies (b \cdot a < c \cdot a \leftrightarrow b < c)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If right multiplication by positive elements is strictly monotone and right multiplication by nonnegative elements reflects the strict order, then for any positive element $a > 0$ and any elements $b, c \in \alpha$, we have the equivalence: \[ b \cdot a < c \cdot a \quad \text{if and only if} \quad b < c. \]

mul_le_mul_left theorem

[PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) : a * b ≤ a * c ↔ b ≤ c

Full source

@[simp]
theorem mul_le_mul_left [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) : a * b ≤ a * c ↔ b ≤ c :=
  @rel_iff_cov α>0 α (fun x y => x * y) (· ≤ ·) _ _ ⟨a, a0⟩ _ _

Left Multiplication by Positive Elements Preserves Order: $a > 0 \implies (a \cdot b \leq a \cdot c \leftrightarrow b \leq c)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by nonnegative elements is monotone (`PosMulMono α`) and left multiplication by positive elements reflects the order (`PosMulReflectLE α`), then for any positive element $a > 0$ and any elements $b, c \in \alpha$, we have the equivalence: \[ a \cdot b \leq a \cdot c \quad \text{if and only if} \quad b \leq c. \]

mul_le_mul_right theorem

[MulPosMono α] [MulPosReflectLE α] (a0 : 0 < a) : b * a ≤ c * a ↔ b ≤ c

Full source

@[simp]
theorem mul_le_mul_right [MulPosMono α] [MulPosReflectLE α] (a0 : 0 < a) : b * a ≤ c * a ↔ b ≤ c :=
  @rel_iff_cov α>0 α (fun x y => y * x) (· ≤ ·) _ _ ⟨a, a0⟩ _ _

Right Multiplication by Positive Elements Preserves and Reflects Order: $a > 0 \implies (b \cdot a \leq c \cdot a \leftrightarrow b \leq c)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If right multiplication by nonnegative elements is monotone and right multiplication by positive elements reflects the non-strict order, then for any positive element $a > 0$ and any elements $b, c \in \alpha$, we have the equivalence: \[ b \cdot a \leq c \cdot a \quad \text{if and only if} \quad b \leq c. \]

mul_le_mul_of_nonneg theorem

[PosMulMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 ≤ d) : a * c ≤ b * d

Full source

theorem mul_le_mul_of_nonneg [PosMulMono α] [MulPosMono α]
    (h₁ : a ≤ b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 ≤ d) : a * c ≤ b * d :=
  (mul_le_mul_of_nonneg_left h₂ a0).trans (mul_le_mul_of_nonneg_right h₁ d0)

Monotonicity of Multiplication by Nonnegative Elements: $a \leq b \land c \leq d \land a \geq 0 \land d \geq 0 \implies a \cdot c \leq b \cdot d$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by nonnegative elements is monotone (`PosMulMono α`) and right multiplication by nonnegative elements is monotone (`MulPosMono α`), then for any elements $a, b, c, d \in \alpha$ with $a \leq b$ and $c \leq d$, and any nonnegative elements $a \geq 0$ and $d \geq 0$, we have $a \cdot c \leq b \cdot d$.

mul_le_mul_of_nonneg' theorem

[PosMulMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c ≤ d) (c0 : 0 ≤ c) (b0 : 0 ≤ b) : a * c ≤ b * d

Full source

theorem mul_le_mul_of_nonneg' [PosMulMono α] [MulPosMono α]
    (h₁ : a ≤ b) (h₂ : c ≤ d) (c0 : 0 ≤ c) (b0 : 0 ≤ b) : a * c ≤ b * d :=
  (mul_le_mul_of_nonneg_right h₁ c0).trans (mul_le_mul_of_nonneg_left h₂ b0)

Monotonicity of Multiplication under Nonnegative Conditions: $a \leq b \land c \leq d \land c \geq 0 \land b \geq 0 \implies a \cdot c \leq b \cdot d$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by nonnegative elements is monotone (`PosMulMono α`) and right multiplication by nonnegative elements is monotone (`MulPosMono α`), then for any elements $a, b, c, d \in \alpha$ with $a \leq b$ and $c \leq d$, and any nonnegative elements $c \geq 0$ and $b \geq 0$, we have $a \cdot c \leq b \cdot d$.

mul_lt_mul_of_le_of_lt_of_pos_of_nonneg theorem

[PosMulStrictMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 ≤ d) : a * c < b * d

Full source

theorem mul_lt_mul_of_le_of_lt_of_pos_of_nonneg [PosMulStrictMono α] [MulPosMono α]
    (h₁ : a ≤ b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 ≤ d) : a * c < b * d :=
  (mul_lt_mul_of_pos_left h₂ a0).trans_le (mul_le_mul_of_nonneg_right h₁ d0)

Strict Inequality under Mixed Multiplication: $a \leq b \land c < d \land a > 0 \land d \geq 0 \implies a \cdot c < b \cdot d$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by positive elements is strictly monotone (`PosMulStrictMono α`) and right multiplication by nonnegative elements is monotone (`MulPosMono α`), then for any elements $a, b, c, d \in \alpha$ with $a \leq b$ and $c < d$, and any positive element $a > 0$ and nonnegative element $d \geq 0$, we have $a \cdot c < b \cdot d$.

mul_lt_mul_of_le_of_lt_of_nonneg_of_pos theorem

[PosMulStrictMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c < d) (c0 : 0 ≤ c) (b0 : 0 < b) : a * c < b * d

Full source

theorem mul_lt_mul_of_le_of_lt_of_nonneg_of_pos [PosMulStrictMono α] [MulPosMono α]
    (h₁ : a ≤ b) (h₂ : c < d) (c0 : 0 ≤ c) (b0 : 0 < b) : a * c < b * d :=
  (mul_le_mul_of_nonneg_right h₁ c0).trans_lt (mul_lt_mul_of_pos_left h₂ b0)

Strict Inequality under Mixed Multiplication: $a \leq b \land c < d \land c \geq 0 \land b > 0 \implies a \cdot c < b \cdot d$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by positive elements is strictly monotone (`PosMulStrictMono α`) and right multiplication by nonnegative elements is monotone (`MulPosMono α`), then for any elements $a, b, c, d \in \alpha$ with $a \leq b$ and $c < d$, and any nonnegative element $c \geq 0$ and positive element $b > 0$, we have $a \cdot c < b \cdot d$.

mul_lt_mul_of_lt_of_le_of_nonneg_of_pos theorem

[PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 < d) : a * c < b * d

Full source

theorem mul_lt_mul_of_lt_of_le_of_nonneg_of_pos [PosMulMono α] [MulPosStrictMono α]
    (h₁ : a < b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 < d) : a * c < b * d :=
  (mul_le_mul_of_nonneg_left h₂ a0).trans_lt (mul_lt_mul_of_pos_right h₁ d0)

Strict Inequality Preservation under Mixed Multiplication: $a 0 \implies a \cdot c < b \cdot d$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by nonnegative elements is monotone (`PosMulMono α`) and right multiplication by positive elements is strictly monotone (`MulPosStrictMono α`), then for any elements $a, b, c, d \in \alpha$ with $a < b$ and $c \leq d$, and any nonnegative element $a \geq 0$ and positive element $d > 0$, we have $a \cdot c < b \cdot d$.

mul_lt_mul_of_lt_of_le_of_pos_of_nonneg theorem

[PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c ≤ d) (c0 : 0 < c) (b0 : 0 ≤ b) : a * c < b * d

Full source

theorem mul_lt_mul_of_lt_of_le_of_pos_of_nonneg [PosMulMono α] [MulPosStrictMono α]
    (h₁ : a < b) (h₂ : c ≤ d) (c0 : 0 < c) (b0 : 0 ≤ b) : a * c < b * d :=
  (mul_lt_mul_of_pos_right h₁ c0).trans_le (mul_le_mul_of_nonneg_left h₂ b0)

Strict inequality under mixed multiplication with positive and nonnegative elements: $a 0 \land b \geq 0 \implies a \cdot c < b \cdot d$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by nonnegative elements is monotone (`PosMulMono α`) and right multiplication by positive elements is strictly monotone (`MulPosStrictMono α`), then for any elements $a, b, c, d \in \alpha$ with $a < b$ and $c \leq d$, and any positive element $c > 0$ and nonnegative element $b \geq 0$, we have $a \cdot c < b \cdot d$.

mul_lt_mul_of_pos theorem

[PosMulStrictMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 < d) : a * c < b * d

Full source

theorem mul_lt_mul_of_pos [PosMulStrictMono α] [MulPosStrictMono α]
    (h₁ : a < b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 < d) : a * c < b * d :=
  (mul_lt_mul_of_pos_left h₂ a0).trans (mul_lt_mul_of_pos_right h₁ d0)

Strict Inequality Preservation under Multiplication with Positive Elements: $a 0 \land d > 0 \implies a \cdot c < b \cdot d$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by positive elements is strictly monotone (`PosMulStrictMono α`) and right multiplication by positive elements is strictly monotone (`MulPosStrictMono α`), then for any elements $a, b, c, d \in \alpha$ with $a < b$ and $c < d$, and any positive elements $a > 0$ and $d > 0$, we have $a \cdot c < b \cdot d$.

mul_lt_mul_of_pos' theorem

[PosMulStrictMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c < d) (c0 : 0 < c) (b0 : 0 < b) : a * c < b * d

Full source

theorem mul_lt_mul_of_pos' [PosMulStrictMono α] [MulPosStrictMono α]
    (h₁ : a < b) (h₂ : c < d) (c0 : 0 < c) (b0 : 0 < b) : a * c < b * d :=
  (mul_lt_mul_of_pos_right h₁ c0).trans (mul_lt_mul_of_pos_left h₂ b0)

Strict Inequality Preservation under Multiplication with Positive Elements (Variant): $a 0 \land b > 0 \implies a \cdot c < b \cdot d$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by positive elements is strictly monotone (`PosMulStrictMono α`) and right multiplication by positive elements is strictly monotone (`MulPosStrictMono α`), then for any elements $a, b, c, d \in \alpha$ with $a < b$ and $c < d$, and any positive elements $c > 0$ and $b > 0$, we have $a \cdot c < b \cdot d$.

mul_le_of_mul_le_of_nonneg_left theorem

[PosMulMono α] (h : a * b ≤ c) (hle : d ≤ b) (a0 : 0 ≤ a) : a * d ≤ c

Full source

theorem mul_le_of_mul_le_of_nonneg_left [PosMulMono α] (h : a * b ≤ c) (hle : d ≤ b) (a0 : 0 ≤ a) :
    a * d ≤ c :=
  (mul_le_mul_of_nonneg_left hle a0).trans h

Left Multiplication Monotonicity for Nonnegative Elements: $a \geq 0 \land d \leq b \implies a \cdot d \leq c$ given $a \cdot b \leq c$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by nonnegative elements is monotone (i.e., the typeclass `PosMulMono α` holds). For any elements $a, b, c, d \in \alpha$ such that $a \cdot b \leq c$, $d \leq b$, and $a \geq 0$, we have $a \cdot d \leq c$.

mul_lt_of_mul_lt_of_nonneg_left theorem

[PosMulMono α] (h : a * b < c) (hle : d ≤ b) (a0 : 0 ≤ a) : a * d < c

Full source

theorem mul_lt_of_mul_lt_of_nonneg_left [PosMulMono α] (h : a * b < c) (hle : d ≤ b) (a0 : 0 ≤ a) :
    a * d < c :=
  (mul_le_mul_of_nonneg_left hle a0).trans_lt h

Strict Inequality Preservation under Left Multiplication by Nonnegative Elements: $a \cdot b < c \land d \leq b \land a \geq 0 \implies a \cdot d < c$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by nonnegative elements is monotone (i.e., the typeclass `PosMulMono α` holds). For any elements $a, b, c, d \in \alpha$ such that $a \cdot b < c$, $d \leq b$, and $a \geq 0$, we have $a \cdot d < c$.

le_mul_of_le_mul_of_nonneg_left theorem

[PosMulMono α] (h : a ≤ b * c) (hle : c ≤ d) (b0 : 0 ≤ b) : a ≤ b * d

Full source

theorem le_mul_of_le_mul_of_nonneg_left [PosMulMono α] (h : a ≤ b * c) (hle : c ≤ d) (b0 : 0 ≤ b) :
    a ≤ b * d :=
  h.trans (mul_le_mul_of_nonneg_left hle b0)

Inequality Preservation under Left Multiplication by Nonnegative Elements: $a \leq b \cdot c \land c \leq d \land b \geq 0 \implies a \leq b \cdot d$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by nonnegative elements is monotone (i.e., `PosMulMono α` holds). For any elements $a, b, c, d \in \alpha$ such that $a \leq b \cdot c$, $c \leq d$, and $0 \leq b$, it follows that $a \leq b \cdot d$.

lt_mul_of_lt_mul_of_nonneg_left theorem

[PosMulMono α] (h : a < b * c) (hle : c ≤ d) (b0 : 0 ≤ b) : a < b * d

Full source

theorem lt_mul_of_lt_mul_of_nonneg_left [PosMulMono α] (h : a < b * c) (hle : c ≤ d) (b0 : 0 ≤ b) :
    a < b * d :=
  h.trans_le (mul_le_mul_of_nonneg_left hle b0)

Strict Inequality Preservation under Left Multiplication by Nonnegative Elements: $a < b \cdot c \land c \leq d \land b \geq 0 \implies a < b \cdot d$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by nonnegative elements is monotone (i.e., `PosMulMono α` holds). For any elements $a, b, c, d \in \alpha$ such that $a < b \cdot c$, $c \leq d$, and $0 \leq b$, it follows that $a < b \cdot d$.

mul_le_of_mul_le_of_nonneg_right theorem

[MulPosMono α] (h : a * b ≤ c) (hle : d ≤ a) (b0 : 0 ≤ b) : d * b ≤ c

Full source

theorem mul_le_of_mul_le_of_nonneg_right [MulPosMono α] (h : a * b ≤ c) (hle : d ≤ a) (b0 : 0 ≤ b) :
    d * b ≤ c :=
  (mul_le_mul_of_nonneg_right hle b0).trans h

Inequality Preservation under Right Multiplication by Nonnegative Elements: $a \cdot b \leq c \land d \leq a \land b \geq 0 \implies d \cdot b \leq c$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by nonnegative elements is monotone (i.e., `MulPosMono α` holds). For any elements $a, b, c, d \in \alpha$ such that $a \cdot b \leq c$, $d \leq a$, and $0 \leq b$, it follows that $d \cdot b \leq c$.

mul_lt_of_mul_lt_of_nonneg_right theorem

[MulPosMono α] (h : a * b < c) (hle : d ≤ a) (b0 : 0 ≤ b) : d * b < c

Full source

theorem mul_lt_of_mul_lt_of_nonneg_right [MulPosMono α] (h : a * b < c) (hle : d ≤ a) (b0 : 0 ≤ b) :
    d * b < c :=
  (mul_le_mul_of_nonneg_right hle b0).trans_lt h

Strict Inequality Preservation under Left Multiplication by Nonnegative Elements: $a \cdot b < c \land d \leq a \land b \geq 0 \implies d \cdot b < c$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by nonnegative elements is monotone (i.e., `MulPosMono α` holds). For any elements $a, b, c, d \in \alpha$ such that $a \cdot b < c$, $d \leq a$, and $0 \leq b$, it follows that $d \cdot b < c$.

le_mul_of_le_mul_of_nonneg_right theorem

[MulPosMono α] (h : a ≤ b * c) (hle : b ≤ d) (c0 : 0 ≤ c) : a ≤ d * c

Full source

theorem le_mul_of_le_mul_of_nonneg_right [MulPosMono α] (h : a ≤ b * c) (hle : b ≤ d) (c0 : 0 ≤ c) :
    a ≤ d * c :=
  h.trans (mul_le_mul_of_nonneg_right hle c0)

Inequality Preservation under Right Multiplication by Nonnegative Elements: $a \leq b \cdot c \land b \leq d \land c \geq 0 \implies a \leq d \cdot c$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by nonnegative elements is monotone (i.e., `MulPosMono α` holds). For any elements $a, b, c, d \in \alpha$ such that $a \leq b \cdot c$, $b \leq d$, and $0 \leq c$, it follows that $a \leq d \cdot c$.

lt_mul_of_lt_mul_of_nonneg_right theorem

[MulPosMono α] (h : a < b * c) (hle : b ≤ d) (c0 : 0 ≤ c) : a < d * c

Full source

theorem lt_mul_of_lt_mul_of_nonneg_right [MulPosMono α] (h : a < b * c) (hle : b ≤ d) (c0 : 0 ≤ c) :
    a < d * c :=
  h.trans_le (mul_le_mul_of_nonneg_right hle c0)

Strict Inequality Preservation under Right Multiplication by Nonnegative Elements: $a < b \cdot c \land b \leq d \land c \geq 0 \implies a < d \cdot c$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by nonnegative elements is monotone (i.e., `MulPosMono α` holds). For any elements $a, b, c, d \in \alpha$ such that $a < b \cdot c$, $b \leq d$, and $0 \leq c$, it follows that $a < d \cdot c$.

posMulMono_iff_mulPosMono theorem

: PosMulMono α ↔ MulPosMono α

Full source

theorem posMulMono_iff_mulPosMono : PosMulMonoPosMulMono α ↔ MulPosMono α := by
  simp only [posMulMono_iff, mulPosMono_iff, Std.Commutative.comm]

Equivalence of Left and Right Multiplication Monotonicity by Nonnegative Elements

Informal description

For a preorder $\alpha$, the property that left multiplication by nonnegative elements is monotone is equivalent to the property that right multiplication by nonnegative elements is monotone. That is, the following are equivalent: 1. For any $b \geq 0$ and $a_1 \leq a_2$, we have $b \cdot a_1 \leq b \cdot a_2$. 2. For any $b \geq 0$ and $a_1 \leq a_2$, we have $a_1 \cdot b \leq a_2 \cdot b$.

PosMulMono.toMulPosMono theorem

[PosMulMono α] : MulPosMono α

Full source

theorem PosMulMono.toMulPosMono [PosMulMono α] : MulPosMono α := posMulMono_iff_mulPosMono.mp ‹_›

Monotonicity of Right Multiplication Implied by Left Multiplication Monotonicity

Informal description

If left multiplication by nonnegative elements in a preorder $\alpha$ is monotone, then right multiplication by nonnegative elements in $\alpha$ is also monotone. That is, if for any $b \geq 0$ and $a_1 \leq a_2$ we have $b \cdot a_1 \leq b \cdot a_2$, then for any $b \geq 0$ and $a_1 \leq a_2$ we also have $a_1 \cdot b \leq a_2 \cdot b$.

posMulStrictMono_iff_mulPosStrictMono theorem

: PosMulStrictMono α ↔ MulPosStrictMono α

Full source

theorem posMulStrictMono_iff_mulPosStrictMono : PosMulStrictMonoPosMulStrictMono α ↔ MulPosStrictMono α := by
  simp only [posMulStrictMono_iff, mulPosStrictMono_iff, Std.Commutative.comm]

Equivalence of Strict Monotonicity for Left and Right Multiplication by Positive Elements

Informal description

For a preorder $\alpha$, left multiplication by positive elements is strictly monotone if and only if right multiplication by positive elements is strictly monotone. That is, the following are equivalent: 1. For any $b > 0$ in $\alpha$, if $a_1 < a_2$, then $b \cdot a_1 0$ in $\alpha$, if $a_1 < a_2$, then $a_1 \cdot b < a_2 \cdot b$.

PosMulStrictMono.toMulPosStrictMono theorem

[PosMulStrictMono α] : MulPosStrictMono α

Full source

theorem PosMulStrictMono.toMulPosStrictMono [PosMulStrictMono α] : MulPosStrictMono α :=
  posMulStrictMono_iff_mulPosStrictMono.mp ‹_›

Strict Monotonicity of Left Multiplication Implies Strict Monotonicity of Right Multiplication for Positive Elements

Informal description

If left multiplication by positive elements in a preorder $\alpha$ is strictly monotone (i.e., for any $b > 0$ and $a_1 < a_2$, we have $b \cdot a_1 0$ and $a_1 < a_2$, we have $a_1 \cdot b < a_2 \cdot b$).

posMulReflectLE_iff_mulPosReflectLE theorem

: PosMulReflectLE α ↔ MulPosReflectLE α

Full source

theorem posMulReflectLE_iff_mulPosReflectLE : PosMulReflectLEPosMulReflectLE α ↔ MulPosReflectLE α := by
  simp only [posMulReflectLE_iff, mulPosReflectLE_iff, Std.Commutative.comm]

Equivalence of left and right multiplication order reflection by positive elements

Informal description

For a preorder $\alpha$, the following are equivalent: 1. For any positive element $b > 0$ in $\alpha$, left multiplication by $b$ reflects the non-strict order relation (i.e., $b \cdot a_1 \leq b \cdot a_2$ implies $a_1 \leq a_2$). 2. For any positive element $b > 0$ in $\alpha$, right multiplication by $b$ reflects the non-strict order relation (i.e., $a_1 \cdot b \leq a_2 \cdot b$ implies $a_1 \leq a_2$).

PosMulReflectLE.toMulPosReflectLE theorem

[PosMulReflectLE α] : MulPosReflectLE α

Full source

theorem PosMulReflectLE.toMulPosReflectLE [PosMulReflectLE α] : MulPosReflectLE α :=
  posMulReflectLE_iff_mulPosReflectLE.mp ‹_›

Left multiplication order reflection implies right multiplication order reflection for positive elements

Informal description

If left multiplication by positive elements in a preorder $\alpha$ reflects the non-strict order relation (i.e., for any $b > 0$ in $\alpha$, $b \cdot a_1 \leq b \cdot a_2$ implies $a_1 \leq a_2$), then right multiplication by positive elements in $\alpha$ also reflects the non-strict order relation (i.e., for any $b > 0$ in $\alpha$, $a_1 \cdot b \leq a_2 \cdot b$ implies $a_1 \leq a_2$).

posMulReflectLT_iff_mulPosReflectLT theorem

: PosMulReflectLT α ↔ MulPosReflectLT α

Full source

theorem posMulReflectLT_iff_mulPosReflectLT : PosMulReflectLTPosMulReflectLT α ↔ MulPosReflectLT α := by
  simp only [posMulReflectLT_iff, mulPosReflectLT_iff, Std.Commutative.comm]

Equivalence of left and right multiplication reflecting strict order for nonnegative elements

Informal description

For a preorder $\alpha$, the property that left multiplication by nonnegative elements reflects the strict order is equivalent to the property that right multiplication by nonnegative elements reflects the strict order. That is, the following are equivalent: 1. For all $b \geq 0$ in $\alpha$ and $a_1, a_2 \in \alpha$, if $b \cdot a_1 < b \cdot a_2$, then $a_1 < a_2$. 2. For all $b \geq 0$ in $\alpha$ and $a_1, a_2 \in \alpha$, if $a_1 \cdot b < a_2 \cdot b$, then $a_1 < a_2$.

PosMulReflectLT.toMulPosReflectLT theorem

[PosMulReflectLT α] : MulPosReflectLT α

Full source

theorem PosMulReflectLT.toMulPosReflectLT [PosMulReflectLT α] : MulPosReflectLT α :=
  posMulReflectLT_iff_mulPosReflectLT.mp ‹_›

Left multiplication reflecting strict order implies right multiplication reflecting strict order for nonnegative elements

Informal description

For any preorder $\alpha$, if left multiplication by nonnegative elements reflects the strict order (i.e., for all $b \geq 0$ in $\alpha$ and $a_1, a_2 \in \alpha$, $b \cdot a_1 < b \cdot a_2$ implies $a_1 < a_2$), then right multiplication by nonnegative elements also reflects the strict order (i.e., for all $b \geq 0$ in $\alpha$ and $a_1, a_2 \in \alpha$, $a_1 \cdot b < a_2 \cdot b$ implies $a_1 < a_2$).

PosMulStrictMono.toPosMulReflectLE instance

[PosMulStrictMono α] : PosMulReflectLE α

Full source

instance (priority := 100) PosMulStrictMono.toPosMulReflectLE [PosMulStrictMono α] :
    PosMulReflectLE α where
  elim := (covariant_lt_iff_contravariant_le _ _ _).1 CovariantClass.elim

Strict Monotonicity of Left Multiplication Implies Non-Strict Order Reflection

Informal description

For any preorder $\alpha$ where left multiplication by positive elements is strictly monotone (i.e., $a_1 < a_2$ implies $b \cdot a_1 0$), it follows that left multiplication by positive elements also reflects the non-strict order (i.e., $b \cdot a_1 \leq b \cdot a_2$ implies $a_1 \leq a_2$ for $b > 0$).

MulPosStrictMono.toMulPosReflectLE instance

[MulPosStrictMono α] : MulPosReflectLE α

Full source

instance (priority := 100) MulPosStrictMono.toMulPosReflectLE [MulPosStrictMono α] :
    MulPosReflectLE α where
  elim := (covariant_lt_iff_contravariant_le _ _ _).1 CovariantClass.elim

Strict Monotonicity of Right Multiplication Implies Non-Strict Order Reflection

Informal description

For any preorder $\alpha$ where right multiplication by positive elements is strictly monotone (i.e., $a_1 < a_2$ implies $a_1 * b < a_2 * b$ for $b > 0$), it follows that right multiplication by positive elements also reflects the non-strict order (i.e., $a_1 * b \leq a_2 * b$ implies $a_1 \leq a_2$ for $b > 0$).

PosMulReflectLE.toPosMulStrictMono theorem

[PosMulReflectLE α] : PosMulStrictMono α

Full source

theorem PosMulReflectLE.toPosMulStrictMono [PosMulReflectLE α] : PosMulStrictMono α where
  elim := (covariant_lt_iff_contravariant_le _ _ _).2 ContravariantClass.elim

Order Reflection Implies Strict Monotonicity for Left Multiplication by Positive Elements

Informal description

For any preorder $\alpha$, if left multiplication by positive elements reflects the non-strict order (i.e., $b \cdot a_1 \leq b \cdot a_2$ implies $a_1 \leq a_2$ for $b > 0$), then left multiplication by positive elements is strictly monotone (i.e., $a_1 < a_2$ implies $b \cdot a_1 0$).

MulPosReflectLE.toMulPosStrictMono theorem

[MulPosReflectLE α] : MulPosStrictMono α

Full source

theorem MulPosReflectLE.toMulPosStrictMono [MulPosReflectLE α] : MulPosStrictMono α where
  elim := (covariant_lt_iff_contravariant_le _ _ _).2 ContravariantClass.elim

Order reflection implies strict monotonicity for right multiplication by positive elements

Informal description

For any preorder $\alpha$, if right multiplication by positive elements reflects the non-strict order (i.e., $a_1 * b \leq a_2 * b$ implies $a_1 \leq a_2$ for $b > 0$), then right multiplication by positive elements is strictly monotone (i.e., $a_1 < a_2$ implies $a_1 * b < a_2 * b$ for $b > 0$).

posMulStrictMono_iff_posMulReflectLE theorem

: PosMulStrictMono α ↔ PosMulReflectLE α

Full source

theorem posMulStrictMono_iff_posMulReflectLE : PosMulStrictMonoPosMulStrictMono α ↔ PosMulReflectLE α :=
  ⟨@PosMulStrictMono.toPosMulReflectLE _ _ _ _, @PosMulReflectLE.toPosMulStrictMono _ _ _ _⟩

Equivalence of Strict Monotonicity and Non-Strict Order Reflection for Left Multiplication by Positive Elements

Informal description

For a preorder $\alpha$, left multiplication by positive elements is strictly monotone (i.e., $a_1 < a_2$ implies $b \cdot a_1 0$) if and only if it reflects the non-strict order (i.e., $b \cdot a_1 \leq b \cdot a_2$ implies $a_1 \leq a_2$ for all $b > 0$).

mulPosStrictMono_iff_mulPosReflectLE theorem

: MulPosStrictMono α ↔ MulPosReflectLE α

Full source

theorem mulPosStrictMono_iff_mulPosReflectLE : MulPosStrictMonoMulPosStrictMono α ↔ MulPosReflectLE α :=
  ⟨@MulPosStrictMono.toMulPosReflectLE _ _ _ _, @MulPosReflectLE.toMulPosStrictMono _ _ _ _⟩

Equivalence of Strict Monotonicity and Non-Strict Order Reflection for Right Multiplication by Positive Elements

Informal description

For any preorder $\alpha$, right multiplication by positive elements is strictly monotone (i.e., $a_1 < a_2$ implies $a_1 * b < a_2 * b$ for $b > 0$) if and only if it reflects the non-strict order (i.e., $a_1 * b \leq a_2 * b$ implies $a_1 \leq a_2$ for $b > 0$).

PosMulReflectLT.toPosMulMono theorem

[PosMulReflectLT α] : PosMulMono α

Full source

theorem PosMulReflectLT.toPosMulMono [PosMulReflectLT α] : PosMulMono α where
  elim := (covariant_le_iff_contravariant_lt _ _ _).2 ContravariantClass.elim

Strict order reflection implies monotonicity for left multiplication by nonnegative elements

Informal description

If left multiplication by nonnegative elements in a preorder $\alpha$ reflects the strict order (i.e., for any $b \geq 0$, if $b \cdot a_1 < b \cdot a_2$ implies $a_1 < a_2$), then it is also monotone (i.e., for any $b \geq 0$ and $a_1 \leq a_2$, we have $b \cdot a_1 \leq b \cdot a_2$).

MulPosReflectLT.toMulPosMono theorem

[MulPosReflectLT α] : MulPosMono α

Full source

theorem MulPosReflectLT.toMulPosMono [MulPosReflectLT α] : MulPosMono α where
  elim := (covariant_le_iff_contravariant_lt _ _ _).2 ContravariantClass.elim

Strict order reflection implies monotonicity for right multiplication by nonnegative elements

Informal description

If right multiplication by nonnegative elements in a preorder $\alpha$ reflects the strict order (i.e., for any $b \geq 0$, if $a_1 * b < a_2 * b$ implies $a_1 < a_2$), then it is also monotone (i.e., for any $b \geq 0$ and $a_1 \leq a_2$, we have $a_1 * b \leq a_2 * b$).

PosMulMono.toPosMulReflectLT theorem

[PosMulMono α] : PosMulReflectLT α

Full source

theorem PosMulMono.toPosMulReflectLT [PosMulMono α] : PosMulReflectLT α where
  elim := (covariant_le_iff_contravariant_lt _ _ _).1 CovariantClass.elim

Monotonicity of left multiplication by nonnegative elements implies strict order reflection

Informal description

If left multiplication by nonnegative elements in a preorder $\alpha$ is monotone (i.e., for any $b \geq 0$ and $a_1 \leq a_2$, we have $b \cdot a_1 \leq b \cdot a_2$), then it also reflects the strict order (i.e., for any $b \geq 0$, if $b \cdot a_1 < b \cdot a_2$, then $a_1 < a_2$).

MulPosMono.toMulPosReflectLT theorem

[MulPosMono α] : MulPosReflectLT α

Full source

theorem MulPosMono.toMulPosReflectLT [MulPosMono α] : MulPosReflectLT α where
  elim := (covariant_le_iff_contravariant_lt _ _ _).1 CovariantClass.elim

Monotonicity of right multiplication by nonnegative elements implies strict order reflection

Informal description

If right multiplication by nonnegative elements in a preorder $\alpha$ is monotone (i.e., for any $b \geq 0$ and $a_1 \leq a_2$, we have $a_1 * b \leq a_2 * b$), then it also reflects the strict order (i.e., for any $b \geq 0$, if $a_1 * b < a_2 * b$, then $a_1 < a_2$).

posMulMono_iff_posMulReflectLT theorem

: PosMulMono α ↔ PosMulReflectLT α

Full source

theorem posMulMono_iff_posMulReflectLT : PosMulMonoPosMulMono α ↔ PosMulReflectLT α :=
  ⟨@PosMulMono.toPosMulReflectLT _ _ _ _, @PosMulReflectLT.toPosMulMono _ _ _ _⟩

Equivalence of Monotonicity and Strict Order Reflection for Left Multiplication by Nonnegative Elements

Informal description

For a preorder $\alpha$, the following are equivalent: 1. Left multiplication by nonnegative elements is monotone (i.e., for any $b \geq 0$ and $a_1 \leq a_2$, we have $b \cdot a_1 \leq b \cdot a_2$). 2. Left multiplication by nonnegative elements reflects the strict order (i.e., for any $b \geq 0$, if $b \cdot a_1 < b \cdot a_2$, then $a_1 < a_2$).

mulPosMono_iff_mulPosReflectLT theorem

: MulPosMono α ↔ MulPosReflectLT α

Full source

theorem mulPosMono_iff_mulPosReflectLT : MulPosMonoMulPosMono α ↔ MulPosReflectLT α :=
  ⟨@MulPosMono.toMulPosReflectLT _ _ _ _, @MulPosReflectLT.toMulPosMono _ _ _ _⟩

Equivalence of Monotonicity and Strict Order Reflection for Right Multiplication by Nonnegative Elements

Informal description

For a preorder $\alpha$, the following are equivalent: 1. Right multiplication by nonnegative elements is monotone (i.e., for any $b \geq 0$ and $a_1 \leq a_2$, we have $a_1 * b \leq a_2 * b$). 2. Right multiplication by nonnegative elements reflects the strict order (i.e., for any $b \geq 0$, if $a_1 * b < a_2 * b$, then $a_1 < a_2$).