mul' — Mathlib

English

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

Русский

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

LaTeX

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

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 : Antitone f) (hg : Antitone g) : Antitone fun x => f x * g x :=
  fun _ _ h => mul_le_mul' (hf h) (hg h)

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