ofSym_map — Mathlib

English

Relabelling by an equivalence e: σ ≃ τ preserves the partition produced by ofSym: ofSym(s.map e) = ofSym s.

Русский

Перебалансировка меток по эквиваленции e: σ ≃ τ сохраняет разбиение, задаваемое ofSym: ofSym(s.map e) = ofSym s.

LaTeX

$$$\mathrm{ofSym}(s\mapsto e) = \mathrm{ofSym}(s)$$$

Lean4

@[simp]
theorem ofSym_map (e : σ ≃ τ) (s : Sym σ n) : ofSym (s.map e) = ofSym s :=
  by
  simp only [ofSym, Sym.val_eq_coe, Sym.coe_map, mk.injEq]
  rw [Multiset.dedup_map_of_injective e.injective]
  simp only [map_map, Function.comp_apply]
  congr; funext i
  rw [← Multiset.count_map_eq_count' e _ e.injective]

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