apply — Mathlib

English

Evaluation at a fixed index i defines a monotone map from the space of families of monotone maps to π i.

Русский

Оценка по фиксированному индексу i задает монотонное отображение пространства семейств монотонных отображений в π_i.

LaTeX

$$$ \Pi.evalOrderHom(i) : (\forall j, \pi j) \to^o \pi i. $$$

Lean4

/-- Function application `fun f => f a` (for fixed `a`) is a monotone function from the
monotone function space `α →o β` to `β`. See also `Pi.evalOrderHom`. -/
@[simps! -fullyApplied]
def apply (x : α) : (α →o β) →o β :=
  (Pi.evalOrderHom x).comp coeFnHom

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