const_nil

Mathlib.Data.TypeVec

URI: https://scilib.ai/kg/mathlib#TypeVec.const_nil

English

The constant map to x over a 0-length vector equals nilFun.

Русский

Константное отображение в x над нулевой длиной равно nilFun.

LaTeX

$$$$\\mathrm{const}(x, \\alpha) = nilFun.$$$$

Lean4

theorem const_nil {β} (x : β) (α : TypeVec 0) : TypeVec.const x α = nilFun := by ext i : 1; cases i

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

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

Разделы

Аффилиация

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