English
Filtering an attached multiset corresponds to filtering the underlying elements and then reattaching via a map.
Русский
Фильтрация прикреплённого мультисета соответствует фильтрации базовых элементов и повторному присоединению через отображение.
LaTeX
$$$ s.attach.filter p = \\mathrm{map} (\\mathrm{Subtype.map} id \\ \\, \\dots) (s.filter (\\lambda x, \\exists h, p ⟨x,h⟩) .attach) $$$
Lean4
theorem filter_attach' (s : Multiset α) (p : { a // a ∈ s } → Prop) [DecidableEq α] [DecidablePred p] :
s.attach.filter p = (s.filter fun x ↦ ∃ h, p ⟨x, h⟩).attach.map (Subtype.map id fun _ ↦ mem_of_mem_filter) := by
classical
refine Multiset.map_injective Subtype.val_injective ?_
rw [map_filter' _ Subtype.val_injective]
simp only [Function.comp, Subtype.exists, Subtype.map, exists_and_right, exists_eq_right, attach_map_val, map_map, id]
