mul_monotone — Mathlib

English

If f is StrictMono and g is Monotone, and positivity conditions hold, then the product f*g is StrictMono.

Русский

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

LaTeX

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

Lean4

theorem mul_monotone [PosMulMono M₀] [MulPosStrictMono M₀] (hf : StrictMono f) (hg : Monotone g) (hf₀ : ∀ x, 0 ≤ f x)
    (hg₀ : ∀ x, 0 < g x) : StrictMono (f * g) := fun _ _ h ↦ mul_lt_mul (hf h) (hg h.le) (hg₀ _) (hf₀ _)

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