const — Mathlib

English

There is a constant n-ary function with value b: OfArity α β n, b ↦ constant function.

Русский

Существуют константные n-арные функции: OfArity.const α b n возвращает константную функцию значением b.

LaTeX

$$$$\mathrm{OfArity.const}(\alpha,\beta,b,n) = \mathrm{FromTypes}.const (\lambda _ : \mathbb{Fin}(n), \alpha)\, b.$$$$

Lean4

/-- Constant `n`-ary function with value `b`. -/
def const (α : Type u) {β : Type u} (b : β) (n : ℕ) : OfArity α β n :=
  FromTypes.const (fun _ => α) b

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