onDiag — Mathlib

English

Restriction of a monotone map f: α →o α →o β to the diagonal yields a monotone map α →o β given by a ↦ f a (a).

Русский

Ограничение монотонного отображения f: α →o α →o β к диагонали дает монотонное отображение α →o β, определяемое как a ↦ f(a)(a).

LaTeX

$$$ onDiag(f)(a)= (f\,a)(a). $$$

Lean4

/-- Restriction of `f : α →o α →o β` to the diagonal. -/
@[simps! +simpRhs]
def onDiag (f : α →o α →o β) : α →o β :=
  (curry.symm f).comp diag

Похожие утверждения