English
There exists a monotone map compₘ that takes a pair of bundled monotone maps f : β →o γ and g : α →o β and returns the bundled monotone map α →o γ given by composing f and g. This map is monotone in each argument.
Русский
Существует монотонное отображение compₘ, которое принимает пару упакованных монотонных отображений f : β →o γ и g : α →o β и возвращает упакованное монотонное отображение α →o γ, заданное композицией f и g. Это отображение монотонно по каждому аргументу.
LaTeX
$$$ comp\_m(f,g) = f \circ g, \quad \text{monotone in } f,g. $$$$
Lean4
/-- The composition of two bundled monotone functions, a fully bundled version. -/
@[simps! -fullyApplied]
def compₘ : (β →o γ) →o (α →o β) →o α →o γ :=
curry ⟨fun f : (β →o γ) × (α →o β) => f.1.comp f.2, fun _ _ h => comp_mono h.1 h.2⟩
