const — Mathlib

English

The constant function with value n is a polynomial: const(n) maps every input to n.

Русский

Постоянная функция, для которой значение равно n, является полиномом: const(n) отображает любой ввод в n.

LaTeX

$$$\text{const}(n) : Poly \alpha \quad$ и $\text{const}(n)(x) = n$ для всех x.$$

Lean4

/-- The constant function with value `n : ℤ`. -/
def const (n : ℤ) : Poly α :=
  ⟨_, IsPoly.const n⟩

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