filter_erase — Mathlib

English

Let p be a predicate, a an element, and S a finite set. Then filtering after erasing a from S equals erasing a from the filtered S: filter p (erase S a) = erase (filter p S) a.

Русский

Пусть p — предикат, a — элемент, S — конечное множество. Тогда фильтрация после стирания a из S равна стиранию a из отфильтрованного S.

LaTeX

$$$\\operatorname{filter}_p(\\operatorname{erase} S a) = \\operatorname{erase}(\\operatorname{filter}_p S) a$$$

Lean4

theorem filter_erase (a : α) (s : Finset α) : filter p (erase s a) = erase (filter p s) a := by grind

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