filter — Mathlib

English

Define a filter operation on Finset: it selects elements of s that satisfy a predicate p.

Русский

Определим операцию фильтра на Finset: выбираются элементы s, удовлетворяющие предикату p.

LaTeX

$$$\\text{filter}(s,p) \\text{ is the subset of } s \\text{ consisting of elements satisfying } p.$$$

Lean4

/-- `Finset.filter p s` is the set of elements of `s` that satisfy `p`.

For example, one can use `s.filter (· ∈ t)` to get the intersection of `s` with `t : Set α`
as a `Finset α` (when a `DecidablePred (· ∈ t)` instance is available). -/
def filter (s : Finset α) : Finset α :=
  ⟨_, s.2.filter p⟩

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