app

Mathlib.Tactic.FunProp.Mor

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.FunProp.Mor.app

Lean4

/-- Morphism application -/
def app (f : Expr) (arg : Arg) : Expr :=
  match arg.coe with
  | none => f.app arg.expr
  | some coe => (coe.app f).app arg.expr

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru