const_append1 — Mathlib

English

The constant map distributes over concatenation: const x applied to α ::: β equals appendFun (const x α) (λ _ => x).

Русский

Постоянное отображение над конкатенацией распределяется как appendFun (const x α) (λ _ => x).

LaTeX

$$$$\\mathrm{const}(x, \\alpha ::: \\beta) = \\mathrm{appendFun}(\\mathrm{const}(x, \\alpha), (\\lambda\\_, x) -> x).$$$$

Lean4

theorem const_append1 {β γ} (x : γ) {n} (α : TypeVec n) :
    TypeVec.const x (α ::: β) = appendFun (TypeVec.const x α) fun _ => x := by ext i : 1; cases i <;> rfl

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