appendFun_id_id — Mathlib

English

The concatenation of identity arrows on α and on β is the identity on the concatenated object α ::: β; equivalently, (TypeVec.id n α ::: id β) = TypeVec.id.

Русский

Соединение единичных морфизмов на α и на β равно единице на объединённом векторе α ::: β; то есть (TypeVec.id n α ::: id β) = TypeVec.id.

LaTeX

$$$$\\big(\\text{TypeVec.appendFun}(\\text{TypeVec.id}, \\text{id})\\big) = \\text{TypeVec.id}.$$$$

Lean4

theorem appendFun_id_id {α : TypeVec n} {β : Type*} : (@TypeVec.id n α ::: @_root_.id β) = TypeVec.id :=
  eq_of_drop_last_eq rfl rfl

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