English
For a finite set s with a predicate p on its elements, the attached filtered set is equal to the filtered attachment via a canonical map between the subtype and s.
Русский
Для конечного множества s с предикатом p на элементы, фильтрованное присоединение эквивалентно образу через естественную отображение подтипа.
LaTeX
$$$ s.\attach.filter p = (s.filter p).attach.map (\\langle \\mathrm{Subtype.map} id \\mid \\mathrm{filter_subset} \\_, \\mathrm{Subtype.map_injective} \\_\\rangle) $$$
Lean4
theorem filter_attach' [DecidableEq α] (s : Finset α) (p : s → Prop) [DecidablePred p] :
s.attach.filter p =
(s.filter fun x => ∃ h, p ⟨x, h⟩).attach.map
⟨Subtype.map id <| filter_subset _ _, Subtype.map_injective _ injective_id⟩ :=
eq_of_veq <| Multiset.filter_attach' _ _
