filter_val — Mathlib

English

The multiset underlying a Finset after filtering by p is the same as filtering the underlying multiset.

Русский

Мультисетное представление конечного множества после фильтрации по p совпадает с фильтрацией соответствующего мультисета.

LaTeX

$$$ (s.filter p).val = \\mathrm{Multiset.filter}\ p\ s.val $$$

Lean4

@[simp]
theorem filter_val (s : Finset α) : (filter p s).1 = s.1.filter p :=
  rfl

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