mul_left_strictMono — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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