const_succ — Mathlib

English

The constant function of arity n+1 is equal to the constant function of arity n, ignoring the new head argument.

Русский

Постоянная функция арности n+1 эквивалентна постоянной функции арности n, игнорирующей новый первый аргумент.

LaTeX

$$$$\mathrm{const}_{n+1}(p, t) = \lambda _ , \mathrm{const}_{n}(\mathrm{vecTail}(p), t). $$$$

Lean4

@[simp]
theorem const_succ {n} (p : Fin (n + 1) → Type u) {τ : Type u} (t : τ) : const p t = fun _ => const (vecTail p) t :=
  rfl

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