English
For any α, β, a fixed b ∈ β and any natural n and x ∈ α, the (n+1)-ary constant function with value b evaluated at x equals the n-ary constant function with value b; i.e., extra input does not affect the constant value.
Русский
Для любых α, β, фиксированного элемента b ∈ β и любого натурального n и элемента x ∈ α константная функция арности n+1 c значением b, применяемая к x, равна константной функции арности n той же величины; то есть дополнительный аргумент не влияет на результат.
LaTeX
$$$(\\text{const}_{\\alpha} b)^{(n+1)}(x) = (\\text{const}_{\\alpha} b)^{(n)}$ for all $n, \\alpha, \\beta, b, x$$$
Lean4
theorem const_succ_apply (α : Type u) {β : Type u} (b : β) (n : ℕ) (x : α) : const α b n.succ x = const _ b n :=
FromTypes.const_succ_apply _ b x
