smul_le_smul — Mathlib

English

If f1 ≤ f2 and g1 ≤ g2, then f1 • g1 ≤ f2 • g2; i.e., the product is monotone in both factors.

Русский

Если f1 ≤ f2 и g1 ≤ g2, то f1 • g1 ≤ f2 • g2; т.е. произведение монотонно по обеим переменным.

LaTeX

$$$f_1 \le f_2 \quad\&\quad g_1 \le g_2 \quad\Rightarrow\quad f_1 \cdot g_1 \le f_2 \cdot g_2$$$

Lean4

@[to_additive]
theorem smul_le_smul : f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ • g₁ ≤ f₂ • g₂ :=
  map₂_mono

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