English
For a list l and a predicate p on elements of the attachment (p : {a | a ∈ l} → Bool), filtering the attached list by p equals mapping the filtered base list after attaching, i.e., a correspondence between filtering attachments and attaching after filtering.
Русский
Для списка l и предиката p на элементы прикрепления (p : {a | a ∈ l} → Bool) фильтрация прикрепленного списка по p эквивалентна отображению отфильтрованного списка после присоединения.
LaTeX
$$$$\operatorname{filter} p\, l\text{.attach} = \operatorname{attach}\big(\operatorname{filter}\big(\lambda x. \exists h, p \langle x, h \rangle\big)\, l\big).\operatorname{map}(\operatorname{Subtype.map} id\, \text{(mem_of_mem_filter)})$$$$
Lean4
theorem filter_attach' (l : List α) (p : { a // a ∈ l } → Bool) [DecidableEq α] :
l.attach.filter p = (l.filter fun x => ∃ h, p ⟨x, h⟩).attach.map (Subtype.map id fun _ => mem_of_mem_filter) := by
classical
refine map_injective_iff.2 Subtype.coe_injective ?_
simp [comp_def, map_filter _ Subtype.coe_injective]
