appendFun_comp_id — Mathlib

English

Appending an identity at the left distributes over composition of right parts: (@id α ::: g1 ∘ g0) equals (id ::: g1) ∘ (id ::: g0).

Русский

Добавление единицы слева через композицию правых частей: (@id α ::: g1 ∘ g0) = (id ::: g1) ∘ (id ::: g0).

LaTeX

$$$(@id_{\alpha} \; ::: \; g_{1} \circ g_{0}) = (id_{\alpha} ::: g_{1}) \circ (id_{\alpha} ::: g_{0})$$$

Lean4

theorem appendFun_comp_id {α : TypeVec n} {β₀ β₁ β₂ : Type u} (g₀ : β₀ → β₁) (g₁ : β₁ → β₂) :
    (@id _ α ::: g₁ ∘ g₀) = (id ::: g₁) ⊚ (id ::: g₀) :=
  eq_of_drop_last_eq rfl rfl

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