fst_mk

Mathlib.Data.Prod.TProd

URI: https://scilib.ai/kg/mathlib#List.TProd.fst_mk

English

The first projection of the constructed iterated product from a head i and tail l is the value at i, i.e., fst(List.TProd.mk(i :: l) f) = f(i).

Русский

Первая компонентаList.TProd.mk(i :: l) равна f(i).

LaTeX

$$$\\mathrm{fst}(\\mathrm{List.TProd.mk}(i::l,f)) = f(i).$$$

Lean4

@[simp]
theorem fst_mk (i : ι) (l : List ι) (f : ∀ i, α i) : (TProd.mk (i :: l) f).1 = f i :=
  rfl

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

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

Разделы

Аффилиация

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