Pi

Mathlib.Data.QPF.Multivariate.Constructions.Sigma

URI: https://scilib.ai/kg/mathlib#MvQPF.Pi

← MathLib Explorer

English

Pi is the dependent product over A of the n-ary functor: Pi F v = ∀ α : A, F α v.

Русский

Pi — зависимый произведение над A полиномиального функторa: Pi F v = ∀ α ∈ A, F α v.

LaTeX

$$$\\\\Pi(v) = ∀ α : A, F(α, v).$$$

Lean4

/-- Dependent product of an `n`-ary functor. The sum can range over
data types like `ℕ` or over `Type.{u-1}` -/
def Pi (v : TypeVec.{u} n) : Type u :=
  ∀ α : A, F α v

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

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

Разделы

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

Аффилиация

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