smul — Mathlib

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) _)

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