mk

Mathlib.Data.Prod.TProd

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

Lean4

/-- Turning a function `f : ∀ i, α i` into an element of the iterated product `TProd α l`. -/
protected def mk : ∀ (l : List ι) (_f : ∀ i, α i), TProd α l
  | [] => fun _ => PUnit.unit
  | i :: is => fun f => (f i, TProd.mk is f)

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

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

Разделы

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

Аффилиация

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