set_prod — Mathlib

English

If f and g are monotone (as set-valued maps), then the map x ↦ f(x) × g(x) is monotone.

Русский

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

LaTeX

$$$ \text{Monotone}(f) \land \text{Monotone}(g) \Rightarrow \text{Monotone}(x \mapsto f(x) \times t g(x)) $$$

Lean4

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

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