filter_attach — Mathlib

English

The attach of a filtered multiset relates to attaching and mapping from the filtered set to the original via membership.

Русский

Прикрепление attach после фильтрации связано с прикреплением и отображением через членство.

LaTeX

$$$\text{filter_attach}(s) = \text{Attach}(\text{filtered}(s))$$$

Lean4

theorem filter_attach (s : Multiset α) (p : α → Prop) [DecidablePred p] :
    (s.attach.filter fun a : { a // a ∈ s } ↦ p ↑a) =
      (s.filter p).attach.map (Subtype.map id fun _ ↦ Multiset.mem_of_mem_filter) :=
  Quotient.inductionOn s fun l ↦ congr_arg _ (List.filter_attach l p)

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