English
A function h from a product is antitone iff it is antitone in each coordinate.
Русский
Функция h из произведения антитонна тогда и только тогда, когда она антитонна по каждой координате.
LaTeX
$$$\text{Antitone } h \iff (\forall a, \text{Antitone } (\lambda b, h(a,b))) \land (\forall b, \text{Antitone } (\lambda a, h(a,b))).$$$
Lean4
theorem antitone_prod_iff {h : α × β → γ} :
Antitone h ↔ (∀ a, Antitone (fun b => h (a, b))) ∧ (∀ b, Antitone (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)
