map_id — Mathlib

English

For finite X, the map induced by the identity on X is the identity on the function space X → M.

Русский

Для конечного множества X индуцированное отображение по единице на X совпадает с тождественным отображением на пространстве функций X → M.

LaTeX

$$$\operatorname{map}(\mathrm{id}_X) = \mathrm{id}_{X \to M}$$$

Lean4

theorem map_id [Finite X] : map (_root_.id : X → X) (M := M) = _root_.id :=
  by
  ext s
  simp [map]

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