English
Let S be a finite set and p a predicate on the ambient type. Then the underlying set of the filtered finite set S.filter p is exactly the set of elements of S that satisfy p; i.e. the coercion of S.filter p to a Set equals { x in S | p x }. In particular, every element of S with p holds appears in the filtered set, and no element not in S appears.
Русский
Пусть S — конечное множество и p — предикат на исходном множестве. Тогда множество, лежащее в основе S.filter p, совпадает с множеством элементов S, удовлетворяющих p; то есть отображение S.filter p в множество равно { x ∈ S | p x }. Все элементы S, для которых выполняется p, входят в фильтр, остальные — нет.
LaTeX
$$$\\uparrow (s \\text{ filter } p) = \\{ x \\in \\uparrow s \\mid p\,x \\}$$$
Lean4
@[simp, norm_cast]
theorem coe_filter (s : Finset α) : ↑(s.filter p) = ({x ∈ ↑s | p x} : Set α) :=
Set.ext fun _ => mem_filter
