apply — Mathlib

English

Casts a multi-tiered constructor to a base function: the composed nested mk yields f.

Русский

Преобразование конструирования через mk в базовую функцию: вложенная композиция выдаёт f.

LaTeX

$$$\\text{coe\_mks} \\; {f} (h_0,h_1,h_2,h_3,h_4,h_5) : = f$$$

Lean4

/-- See Note [custom simps projection] -/
def apply {R α β : Type*} [CommSemiring R] [Semiring α] [Algebra R α] [Semiring β] [Algebra R β] [CoalgebraStruct R α]
    [CoalgebraStruct R β] (f : α →ₐc[R] β) : α → β :=
  f

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