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 monotone_prod_iff {h : α × β → γ} :
Monotone h ↔ (∀ a, Monotone (fun b => h (a, b))) ∧ (∀ b, Monotone (fun a => h (a, b)))
where
mp h := ⟨fun _ _ _ hab => h (Prod.mk_le_mk_iff_right.mpr hab), fun _ _ _ hab => h (Prod.mk_le_mk_iff_left.mpr hab)⟩
mpr h _ _ hab := le_trans (h.1 _ (Prod.mk_le_mk.mp hab).2) (h.2 _ (Prod.mk_le_mk.mp hab).1)
