mul_strictAnti' — Mathlib

English

If f is strictly antitone and g is antitone, then x ↦ f(x)·g(x) is strictly antitone.

Русский

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

LaTeX

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

Lean4

/-- The product of an antitone function and a strictly antitone function is strictly antitone. -/
@[to_additive add_strictAnti /-- The sum of an antitone function and a strictly antitone function is
    strictly antitone. -/
    ]
theorem mul_strictAnti' [MulLeftStrictMono α] [MulRightMono α] {f g : β → α} (hf : Antitone f) (hg : StrictAnti g) :
    StrictAnti fun x => f x * g x := fun _ _ h => mul_lt_mul_of_le_of_lt (hf h.le) (hg h)

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