filterMap_eq_filter — Mathlib

English

Filtering by a predicate after guard equals guarding the filter by the predicate.

Русский

Фильтрация с помощью guard после filterMap эквивалентна фильтрации через predicate.

LaTeX

$$$\operatorname{filterMap}(\text{guard } p) = \operatorname{filter} p$$$

Lean4

theorem filterMap_eq_filter : filterMap (Option.guard p) = filter p :=
  funext fun s => Quot.inductionOn s fun l => congr_arg ofList <| by rw [← List.filterMap_eq_filter]

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