English
Let f : α → γ and g : β → δ be strictly order-reversing. Then the product-map Pro d.map f g : α × β → γ × δ is strictly order-reversing with respect to the product order.
Русский
Пусть f : α → γ и g : β → δ — строго антиупорядочивающие. Тогда отображение Prod.map f g : α × β → γ × δ строго антиупорядочивает относительно произведённого порядка.
LaTeX
$$$\forall (a, b), (a', b') \in \alpha \times \beta,\ (a, b) < (a', b') \Rightarrow (\mathrm{Prod.map}\ f\ g)(a, b) > (\mathrm{Prod.map}\ f\ g)(a', b').$$$
Lean4
theorem prodMap (hf : StrictAnti f) (hg : StrictAnti g) : StrictAnti (Prod.map f g) := fun a b ↦
by
simp only [Prod.lt_iff]
exact Or.imp (And.imp hf.imp hg.antitone.imp) (And.imp hf.antitone.imp hg.imp)
