MorApplication

Mathlib.Tactic.FunProp.FunctionData

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

Lean4

/-- Type of morphism application. -/
inductive MorApplication where/-- Of the form `⇑f` i.e. missing argument. -/

  | underApplied/-- Of the form `⇑f x` i.e. morphism and one argument is provided. -/

  | exact/-- Of the form `⇑f x y ...` i.e. additional applied arguments `y ...`. -/

  | overApplied/-- Not a morphism application. -/

  | none
  deriving Inhabited, BEq

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

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

Разделы

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

Аффилиация

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