English
Given two monotone maps f: α →o β and g: α →o γ, their product map f.prod g: α →o β × γ sends x to (f(x), g(x). The map is monotone in the product order.
Русский
Для двух монотонных отображений f: α →o β и g: α →o γ их произведение f.prod g: α →o β × γ отправляет x в (f(x), g(x)); отображение монотонно по произведению порядков.
LaTeX
$$$ f:\alpha\to^o\beta,\ g:\alpha\to^o\gamma \implies (f\,\mathrm{prod}\, g): \alpha \to^o \beta \times \gamma,\quad (f\mathrm{prod}g)(x)=(f(x),g(x)). $$$
Lean4
/-- Given two bundled monotone maps `f`, `g`, `f.prod g` is the map `x ↦ (f x, g x)` bundled as a
`OrderHom`. -/
@[simps]
protected def prod (f : α →o β) (g : α →o γ) : α →o β × γ :=
⟨fun x => (f x, g x), fun _ _ h => ⟨f.mono h, g.mono h⟩⟩
