mul — Mathlib

English

If f and g are StrictMono and the nonnegativity conditions hold, then f*g is StrictMono as well.

Русский

Если f и g строго монотонны и соблюдены условия неотрицательности, то произведение f*g также строго монотонно.

LaTeX

$$$\text{StrictMono}(f) \land \text{StrictMono}(g) \land (\forall x, 0 \le f(x)) \land (\forall x, 0 \le g(x)) \Rightarrow \text{StrictMono}(f \cdot g)$$$

Lean4

theorem mul [PosMulStrictMono M₀] [MulPosStrictMono M₀] (hf : StrictMono f) (hg : StrictMono g) (hf₀ : ∀ x, 0 ≤ f x)
    (hg₀ : ∀ x, 0 ≤ g x) : StrictMono (f * g) := fun _ _ h ↦ mul_lt_mul'' (hf h) (hg h) (hf₀ _) (hg₀ _)

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