set_prod — Mathlib

English

If f and g are antitone-on the set s, then x ↦ f(x) × g(x) is also antitone-on the set s.

Русский

Если f и g антимонотонны на s, то x ↦ f(x) × g(x) также антимонотонна на s.

LaTeX

$$$\\bigl(\\operatorname{AntitoneOn} f\\, s\\bigr) \\land \\bigl(\\operatorname{AntitoneOn} g\\, s\\bigr) \\Rightarrow \\operatorname{AntitoneOn}\\bigl(\\lambda x. f(x)\\times g(x)\\bigr)\\, s.$$$

Lean4

theorem _root_.AntitoneOn.set_prod (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => f x ×ˢ g x) s :=
  fun _ ha _ hb h => prod_mono (hf ha hb h) (hg ha hb h)

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