English
There is a fully bundled product operation prodₘ that, given two monotone maps f: α →o β and g: α →o γ, yields a monotone map α →o β × γ between OrderHoms, representing the product in the target category.
Русский
Существует полностью упакованная операция произведения prodₘ, которая по двум монотонным отображениям f: α →o β и g: α →o γ образует монотонное отображение α →o β × γ, представляющее произведение в целевой категории.
LaTeX
$$$ prod\_m : (α \to^o β) \to^o (α \to^o γ) \to^o α \to^o (β \times γ),\; prod\_m(f,g)=f \mathrm{prod} g. $$$
Lean4
/-- Given two bundled monotone maps `f`, `g`, `f.prod g` is the map `x ↦ (f x, g x)` bundled as a
`OrderHom`. This is a fully bundled version. -/
@[simps!]
def prodₘ : (α →o β) →o (α →o γ) →o α →o β × γ :=
curry ⟨fun f : (α →o β) × (α →o γ) => f.1.prod f.2, fun _ _ h => prod_mono h.1 h.2⟩
