filter_map

Mathlib.Data.Finset.Image

URI: https://scilib.ai/kg/mathlib#Finset.filter_map

English

For p : β → Prop, we have (s.map f).filter p = (s.filter (p ∘ f)).map f.

Русский

Для p : β → Prop верно (s.map f).filter p = (s.filter (p ∘ f)).map f.

LaTeX

$$$ (s.map f).filter p = (s.filter (p \circ f)).map f$$$

Lean4

theorem filter_map {p : β → Prop} [DecidablePred p] : (s.map f).filter p = (s.filter (p ∘ f)).map f :=
  eq_of_veq (Multiset.filter_map _ _ _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru