dropFun_appendFun

Mathlib.Data.TypeVec

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

English

Dropping the prefix from the append of f and g recovers f: dropFun (f ::: g) = f.

Русский

Усечение префикса у стрелы, полученной как f ::: g, восстанавливает f: dropFun (f ::: g) = f.

LaTeX

$$$\mathrm{dropFun}(\mathrm{f} ::: \mathrm{g}) = \mathrm{f}$$$

Lean4

@[simp]
theorem dropFun_appendFun {α α' : TypeVec n} {β β' : Type*} (f : α ⟹ α') (g : β → β') : dropFun (f ::: g) = f :=
  rfl

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

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

Разделы

Аффилиация

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