Properties of List.reduceOption
#
In this file we prove basic lemmas about List.reduceOption
.
@[simp]
theorem
List.reduceOption_map
{α : Type u_1}
{β : Type u_2}
{l : List (Option α)}
{f : α → β}
:
(List.map (Option.map f) l).reduceOption = List.map f l.reduceOption