fun₀

Mathlib.Data.Finsupp.Notation

URI: https://scilib.ai/kg/mathlib#Finsupp.fun₀

Lean4

/-- `fun₀ | i => a` is notation for `Finsupp.single i a`, and with multiple match arms,
`fun₀ ... | i => a` is notation for `Finsupp.update (fun₀ ...) i a`.

As a result, if multiple match arms coincide, the last one takes precedence. -/
@[term_parser]
def fun₀ :=
  leading_parser:maxPrec ppAllowUngrouped >> unicodeSymbol "λ₀" "fun₀" (preserveForPP := true) >> fun₀.matchAlts

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

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

Разделы

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

Аффилиация

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