comp_cons — Mathlib

English

Composing a function with cons is the same as cons of the composed parts: g ∘ cons y q = cons (g y) (g ∘ q).

Русский

Составление функции с cons равно cons от составленных частей: g ∘ cons y q = cons (g y) (g ∘ q).

LaTeX

$$$g \\circ \\mathrm{cons}(y,q) = \\mathrm{cons}(g y, g \\circ q)$$$

Lean4

theorem comp_cons {α : Sort*} {β : Sort*} (g : α → β) (y : α) (q : Fin n → α) : g ∘ cons y q = cons (g y) (g ∘ q) :=
  by
  ext j
  by_cases h : j = 0
  · rw [h]
    rfl
  · let j' := pred j h
    have : j'.succ = j := succ_pred j h
    rw [← this, cons_succ, comp_apply, comp_apply, cons_succ]

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