Const — Mathlib

English

The Const functor is constant in its arity: for every n and A, (Const n A)(α) = A for all α, and its action on morphisms is the identity on A.

Русский

Функтор Const константен по арности: для каждого n и A множество (Const n A)(α) равно A для всех α, а отображение на стрелах действует как тождество на A.

LaTeX

$$$ (\mathrm{Const}\; n\; A)(\alpha) = A, \quad \mathrm{Const.map}(f)(a) = a. $$$

Lean4

/-- Constant multivariate functor -/
@[nolint unusedArguments]
def Const (A : Type*) (_v : TypeVec.{u} n) : Type _ :=
  A

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