map_id' — Mathlib

English

Sym.map of the identity function is equal to the original element.

Русский

Образ отображения по тождественному отображению равен исходному элементу.

LaTeX

$$$\\forall s : \\mathrm{Sym}(\\alpha,n), \\mathrm{Sym.map}(\\mathrm{id})(s) = s.$$$

Lean4

/-- Note: `Sym.map_id` is not simp-normal, as simp ends up unfolding `id` with `Sym.map_congr` -/
@[simp]
theorem map_id' {α : Type*} {n : ℕ} (s : Sym α n) : Sym.map (fun x : α => x) s = s := by ext;
  simp only [map, Multiset.map_id', ← val_eq_coe]

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