eq_mk_support

Mathlib.Data.DFinsupp.Defs

URI: https://scilib.ai/kg/mathlib#DFinsupp.eq_mk_support

English

Every finitely supported function f equals the canonical representation mk f.support (i ↦ f(i)).

Русский

Любая конечно поддерживаемая функция f расписывается как каноническое представление mk f.support (i ↦ f(i)).

LaTeX

$$$f = \\mathrm{mk} \\; f.{\\mathrm{support}} \\; (\\lambda i, f i)$$$

Lean4

theorem eq_mk_support (f : Π₀ i, β i) : f = mk f.support fun i => f i := by aesop

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

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

Разделы

Аффилиация

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