mul' — Mathlib

English

The product of two strictly antitone functions is strictly antitone.

Русский

Произведение двух связанных строго антитонных функций строго антитонно.

LaTeX

$$$StrictAnti(f) \to\; StrictAnti(g) \Rightarrow StrictAnti(\lambda x. f(x) \cdot g(x))$$$

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 : StrictAnti f) (hg : StrictAnti g) :
    StrictAnti fun x => f x * g x := fun _ _ ab => mul_lt_mul_of_lt_of_lt (hf ab) (hg ab)

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