comp_snoc — Mathlib

English

Composition with snoc distributes over snoc: g ∘ snoc q y = snoc (g ∘ q) (g y).

Русский

Композиция с snoc распределяет по отношению к snoc: g ∘ snoc q y = snoc (g ∘ q) (g y).

LaTeX

$$$g\\\\circ\\\\operatorname{snoc} q y = \\operatorname{snoc}(g\\\\circ q)(g y)$$$

Lean4

theorem comp_snoc {α : Sort*} {β : Sort*} (g : α → β) (q : Fin n → α) (y : α) : g ∘ snoc q y = snoc (g ∘ q) (g y) :=
  by
  ext j
  by_cases h : j.val < n
  · simp [h, snoc, castSucc_castLT]
  · rw [eq_last_of_not_lt h]
    simp

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