mul' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The product of two antitone functions is antitone. -/
@[to_additive add /-- The sum of two antitone functions is antitone. -/
    ]
theorem mul' [MulLeftMono α] [MulRightMono α] (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
    AntitoneOn (fun x => f x * g x) s := fun _ hx _ hy h => mul_le_mul' (hf hx hy h) (hg hx hy h)

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