coe_map — Mathlib

English

The underlying multiset of the mapped Sym equals the image under f of the original multiset.

Русский

Пусть подмножество отображается, тогда база под множества совпадает с отображением через f.

LaTeX

$$$\\forall {s : \\mathrm{Sym}(\\alpha,n)} {f: \\alpha \\to \\beta},\\ (\\mathrm{Sym.map}(f)(s)).toMultiset = \\mathrm{Multiset.map}(f)(s.toMultiset).$$$

Lean4

@[simp]
theorem coe_map (s : Sym α n) (f : α → β) : ↑(s.map f) = Multiset.map f s :=
  rfl

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