attach_map_val — Mathlib

English

For any multiset s, map Subtype.val over s.attach yields s, i.e., mapping the attached elements by their values recovers the original multiset.

Русский

Для любого мультимножества s отображение Subtype.val над s.attach восстанавливает исходное мультимножество: map Subtype.val s.attach = s.

LaTeX

$$$\\forall s:\\\\mathrm{Multiset}\\\\ \\alpha,\\\\ \\mathrm{Multiset.map\\\\ Subtype.val}\\\\ s.attach = s.$$$

Lean4

@[simp]
theorem attach_map_val (s : Multiset α) : s.attach.map Subtype.val = s :=
  (attach_map_val' _ _).trans s.map_id

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