mul' — Mathlib

English

If hf and hg are strictly antitone on s, then x ↦ f(x) · g(x) is strictly antitone on s.

Русский

Если hf и hg строго антитонны на s, то x ↦ f(x) · g(x) строго антитонно на s.

LaTeX

$$$StrictAntiOn(f,s) \;\&\; StrictAntiOn(g,s) \Rightarrow StrictAntiOn(\lambda x. f(x) \cdot g(x), s)$$$

Lean4

/-- The product of two strictly antitone functions is strictly antitone. -/
@[to_additive add /-- The sum of two strictly antitone functions is strictly antitone. -/
    ]
theorem mul' [MulLeftStrictMono α] [MulRightStrictMono α] (hf : StrictAntiOn f s) (hg : StrictAntiOn g s) :
    StrictAntiOn (fun x => f x * g x) s := fun _ ha _ hb ab => mul_lt_mul_of_lt_of_lt (hf ha hb ab) (hg ha hb ab)

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