English
If f,g are monotone functions, then the pointwise product f(x) • g(x) is monotone.
Русский
Если f и g монотонны, то покомпонентное произведение f(x) • g(x) монотонно по x.
LaTeX
$$Monotone f → Monotone g → Monotone (\lambda x, f(x) • g(x))$$
Lean4
@[to_additive]
theorem smul {γ : Type*} [Preorder G] [Preorder P] [Preorder γ] [SMul G P] [IsOrderedSMul G P] {f : γ → G} {g : γ → P}
(hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x • g x := fun _ _ hab =>
(IsOrderedSMul.smul_le_smul_left _ _ (hg hab) _).trans (IsOrderedSMul.smul_le_smul_right _ _ (hf hab) _)