smul_le_smul_right — Mathlib

English

Similarly, if f1 ≤ f2 then f1 • g ≤ f2 • g; i.e., monotone in the left argument while the right is fixed.

Русский

Аналогично, если f1 ≤ f2, то f1 • g ≤ f2 • g; монотонность по левому аргументу при фиксированном правом.

LaTeX

$$$f_1 \le f_2 \Rightarrow f_1 \cdot g \le f_2 \cdot g$$$

Lean4

@[to_additive]
theorem smul_le_smul_right : f₁ ≤ f₂ → f₁ • g ≤ f₂ • g :=
  map₂_mono_right

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