reduceOption_append — Mathlib

English

Appending two option lists and reducing is the same as reducing each then appending the results.

Русский

Сложение двух списков опций с последующим редуцированием эквивалентно редуцированию каждого и их объединению.

LaTeX

$$$\operatorname{reduceOption}(l \append l') = \operatorname{reduceOption}(l) \append \operatorname{reduceOption}(l')$$$

Lean4

theorem reduceOption_append (l l' : List (Option α)) : (l ++ l').reduceOption = l.reduceOption ++ l'.reduceOption :=
  filterMap_append

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