mul — Mathlib

English

If f and g are monotone on a set s, and nonnegative on s, then their product is monotone on s.

Русский

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

LaTeX

$$$MonotoneOn(f,s) \\\\land MonotoneOn(g,s) \\\\land (\\\\forall x \\\\in s, 0 \\\\le f(x)) \\\\land (\\\\forall x \\\\in s, 0 \\\\le g(x)) \\\\Rightarrow MonotoneOn(f * g, s).$$$

Lean4

theorem mul [PosMulMono M₀] [MulPosMono M₀] {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s)
    (hf₀ : ∀ x ∈ s, 0 ≤ f x) (hg₀ : ∀ x ∈ s, 0 ≤ g x) : MonotoneOn (f * g) s := fun _ ha _ hb h ↦
  mul_le_mul (hf ha hb h) (hg ha hb h) (hg₀ _ ha) (hf₀ _ hb)

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