listFilterMap — Mathlib

English

Filtering a list by a decidable predicate is primitive recursive.

Русский

Фильтрация списка по решаемому предикату является примитивно вычислимой.

LaTeX

$$$\\mathrm{Primrec}\\left( \\lambda L. \\mathrm{List}.\\mathrm{filter}(\\lambda x. p(x))\\,L \\right)$$$

Lean4

theorem listFilterMap {f : α → List β} {g : α → β → Option σ} (hf : Primrec f) (hg : Primrec₂ g) :
    Primrec fun a => (f a).filterMap (g a) :=
  (list_flatMap hf (comp₂ optionToList hg)).of_eq fun _ ↦ Eq.symm <| List.filterMap_eq_flatMap_toList _ _

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