prodMk — Mathlib

English

A function h from a product is monotone iff it is monotone in each coordinate.

Русский

Функция h из произведения монотонна тогда и только тогда, когда она монотонна по каждой координате.

LaTeX

$$$\text{Monotone } h \iff (\forall a, \text{Monotone}(b \mapsto h(a,b))) \land (\forall b, \text{Monotone}(a \mapsto h(a,b))).$$$

Lean4

theorem prodMk {f : γ → α} {g : γ → β} (hf : Monotone f) (hg : Monotone g) : Monotone (fun x => (f x, g x)) :=
  monotone_prodMk_iff.2 ⟨hf, hg⟩

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