filter_filter

Mathlib.Data.Finset.Filter

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

English

Filtering by p and then by q is the same as filtering by p and q together.

Русский

Фильтрация по p затем по q эквивалентна фильтрации по p и q одновременно.

LaTeX

$$$(s.filter p).filter q = s.filter (\\lambda a. p\\ a \\land q\\ a) $$$

Lean4

theorem filter_filter (s : Finset α) : (s.filter p).filter q = s.filter fun a => p a ∧ q a := by grind

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

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

Разделы

Аффилиация

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