id_map — Mathlib

English

For every multivariate functor F and every x ∈ F α, applying the identity on all coordinates leaves x unchanged: map_id(x) = x.

Русский

Для каждого многоизмеренного функторa F и каждого x ∈ F α применение тождественного отображения к каждой координате не меняет x: map_id(x) = x.

LaTeX

$$$$F.map(\\mathrm{id})\\,x = x.$$$$

Lean4

protected theorem id_map {α : TypeVec n} (x : F α) : TypeVec.id <$$> x = x :=
  by
  rw [← abs_repr x, ← abs_map]
  rfl

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