mul_right_strictMono — Mathlib

English

If a ≠ 0 and a ≠ ⊤, then multiplication by a on the right is strictly monotone in the second argument: x < y implies x*a < y*a.

Русский

Если a ≠ 0 и a ≠ ⊤, то умножение справа на a строго монотонно по второму аргументу: x < y ⇒ x·a < y·a.

LaTeX

$$$$\forall a \in \mathbb{N}_\infty,\ a \ne 0 \land a \ne \top \Rightarrow \text{StrictMono}(\lambda x, x \cdot a).$$$$

Lean4

theorem mul_right_strictMono (ha : a ≠ 0) (h_top : a ≠ ⊤) : StrictMono (a * ·) :=
  WithTop.mul_right_strictMono (pos_iff_ne_zero.2 ha) h_top

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