filterMap_eq_flatMap_toList — Mathlib

English

For any f: α → Option β and list l, filtering by f and then mapping is equivalent to flat-mapping f.asList: l.filterMap f = l.flatMap (λ a. (f a).toList).

Русский

Для функции f: α → Option β и списка l фильтрация по f с последующим отображением равна плоскому развёртыванию f: l.filterMap f = l.flatMap (λ a. (f a).toList).

LaTeX

$$$$\operatorname{filterMap} f\, l = \operatorname{flatMap}(\lambda a. (f\ a).toList)\, l.$$$$

Lean4

theorem filterMap_eq_flatMap_toList (f : α → Option β) (l : List α) : l.filterMap f = l.flatMap fun a ↦ (f a).toList :=
  by
  induction l with
    | nil => ?_
    | cons a l ih => ?_ <;>
    simp [filterMap_cons]
  rcases f a <;> simp [ih]

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