mul — Mathlib

English

If f and g are monotone and nonnegative, then their pointwise product f*g is monotone.

Русский

Если функции f и g монотонны и неотрицательны, то их поэлементное произведение f*g монотонно.

LaTeX

$$$Monotone(f) \n\\\\land Monotone(g) \\\\land (\\\\forall x, 0 \\\\le f(x)) \\\\land (\\\\forall x, 0 \\\\le g(x)) \\\\Rightarrow Monotone(f * g).$$$

Lean4

theorem mul [PosMulMono M₀] [MulPosMono M₀] (hf : Monotone f) (hg : Monotone g) (hf₀ : ∀ x, 0 ≤ f x)
    (hg₀ : ∀ x, 0 ≤ g x) : Monotone (f * g) := fun _ _ h ↦ mul_le_mul (hf h) (hg h) (hg₀ _) (hf₀ _)

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