filter_attach — Mathlib

English

The filter of s.attach equals the image under a certain embedding of the attached filtered set.

Русский

Фильтрованное множество s.attach эквивалентно образу через некоторое вложение отфильтрованного множества, присоединённого к подмножеству.

LaTeX

$$$ s.attach.filter (fun a : s \mapsto p a) = (s.filter p).attach.map ((Embedding.refl _).subtypeMap mem_of_mem_filter) $$$

Lean4

theorem filter_attach (p : α → Prop) [DecidablePred p] (s : Finset α) :
    s.attach.filter (fun a : s ↦ p a) = (s.filter p).attach.map ((Embedding.refl _).subtypeMap mem_of_mem_filter) :=
  eq_of_veq <| Multiset.filter_attach _ _

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