mul_left_strictMono — Mathlib

English

Left multiplication is strictly monotone, as soon as order-preserving right-multiplication holds.

Русский

Левое умножение строго монотонно, если правая монотонность сохранения порядка выполняется.

LaTeX

$$$[\text{MulRightMono}(\alpha)]\;\Rightarrow\; \text{StrictMono}(x \mapsto a \cdot x).$$$

Lean4

@[to_additive]
theorem mul_left_strictMono [MulRightStrictMono α] {a : α} : StrictMono (· * a) := fun _ _ h ↦
  mul_lt_mul_right' h
    _
      -- Note: in this section, we use `@[gcongr high]` so that these lemmas have a higher priority than
      -- lemmas like `mul_le_mul_of_nonneg`, which have an extra side condition.

Похожие утверждения