English
If hf is antitone on s and hg is strictly antitone on s, then x ↦ f(x)·g(x) is strictly antitone on s.
Русский
Если hf антитонна на s, а hg строго антитонна на s, то x ↦ f(x)·g(x) строго антитонно на s.
LaTeX
$$$AntitoneOn(f,s) \land StrictAntiOn(g,s) \Rightarrow StrictAntiOn(\lambda x. f(x) \cdot g(x), s)$$$
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 : AntitoneOn f s)
(hg : StrictAntiOn g s) : StrictAntiOn (fun x => f x * g x) s := fun _ hx _ hy h =>
mul_lt_mul_of_le_of_lt (hf hx hy h.le) (hg hx hy h)
