apply — Mathlib

English

The Simps projection from bounded continuous functions to the underlying functions is the identity on the function component; i.e., apply(h) = h for every h.

Русский

Проекция Simps из ограниченно непрерывных функций на соответствующую функцию α → β совпадает с самой функцией на уровне отображения; то есть apply(h) = h для любого h.

LaTeX

$$$ (\text{BoundedContinuousFunction.Simps.apply})(h) = h $$$

Lean4

/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
  because it is a composition of multiple projections. -/
def apply (h : α →ᵇ β) : α → β :=
  h

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