Documentation

Mathlib.Data.List.ReduceOption

Properties of List.reduceOption #

In this file we prove basic lemmas about List.reduceOption.

@[simp]
theorem List.reduceOption_cons_of_some {α : Type u_1} (x : α) (l : List (Option α)) :
(some x :: l).reduceOption = x :: l.reduceOption
@[simp]
theorem List.reduceOption_cons_of_none {α : Type u_1} (l : List (Option α)) :
(none :: l).reduceOption = l.reduceOption
@[simp]
theorem List.reduceOption_nil {α : Type u_1} :
[].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
theorem List.reduceOption_append {α : Type u_1} (l : List (Option α)) (l' : List (Option α)) :
(l ++ l').reduceOption = l.reduceOption ++ l'.reduceOption
theorem List.reduceOption_length_eq {α : Type u_1} {l : List (Option α)} :
l.reduceOption.length = (List.filter Option.isSome l).length
theorem List.length_eq_reduceOption_length_add_filter_none {α : Type u_1} {l : List (Option α)} :
l.length = l.reduceOption.length + (List.filter Option.isNone l).length
theorem List.reduceOption_length_le {α : Type u_1} (l : List (Option α)) :
l.reduceOption.length l.length
theorem List.reduceOption_length_eq_iff {α : Type u_1} {l : List (Option α)} :
l.reduceOption.length = l.length ∀ (x : Option α), x lx.isSome = true
theorem List.reduceOption_length_lt_iff {α : Type u_1} {l : List (Option α)} :
l.reduceOption.length < l.length none l
theorem List.reduceOption_singleton {α : Type u_1} (x : Option α) :
[x].reduceOption = x.toList
theorem List.reduceOption_concat {α : Type u_1} (l : List (Option α)) (x : Option α) :
(l.concat x).reduceOption = l.reduceOption ++ x.toList
theorem List.reduceOption_concat_of_some {α : Type u_1} (l : List (Option α)) (x : α) :
(l.concat (some x)).reduceOption = l.reduceOption.concat x
theorem List.reduceOption_mem_iff {α : Type u_1} {l : List (Option α)} {x : α} :
x l.reduceOption some x l
theorem List.reduceOption_get?_iff {α : Type u_1} {l : List (Option α)} {x : α} :
(∃ (i : ), l.get? i = some (some x)) ∃ (i : ), l.reduceOption.get? i = some x