toFinset_filter — Mathlib

English

Filtering a list and then taking its Finset is equivalent to taking the Finset of the list and filtering by the same predicate.

Русский

Фильтрация списка с последующим преобразованием в Finset эквивалентна преобразованию списка в Finset и фильтрации тем же предикатом.

LaTeX

$$$(l.filter p).toFinset = l.toFinset.filter (\\lambda x. p x)$$$

Lean4

@[simp]
theorem toFinset_filter (s : List α) (p : α → Bool) : (s.filter p).toFinset = s.toFinset.filter (p ·) := by ext;
  simp [List.mem_filter]

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