mul_antitone' — Mathlib

English

If hf is strictly antitone on s and hg is 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

$$$StrictAntiOn(f,s) \land AntitoneOn(g,s) \Rightarrow StrictAntiOn(\lambda x. f(x) \cdot g(x), s)$$$

Lean4

/-- The product of a strictly antitone function and an antitone function is strictly antitone. -/
@[to_additive add_antitone /-- The sum of a strictly antitone function and an antitone function is
    strictly antitone. -/
    ]
theorem mul_antitone' (hf : StrictAntiOn f s) (hg : AntitoneOn g s) : StrictAntiOn (fun x => f x * g x) s :=
  fun _ hx _ hy h => mul_lt_mul_of_lt_of_le (hf hx hy h) (hg hx hy h.le)

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