mul_strictMono — Mathlib

English

If f and g are StrictMono and nonnegative, then their product is StrictMono.

Русский

Если 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_strictMono [PosMulStrictMono M₀] [MulPosMono M₀] (hf : Monotone f) (hg : StrictMono g) (hf₀ : ∀ x, 0 < f x)
    (hg₀ : ∀ x, 0 ≤ g x) : StrictMono (f * g) := fun _ _ h ↦ mul_lt_mul' (hf h.le) (hg h) (hg₀ _) (hf₀ _)

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