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 α))
:
List.reduceOption (some x :: l) = x :: List.reduceOption l
@[simp]
theorem
List.reduceOption_cons_of_none
{α : Type u_1}
(l : List (Option α))
:
List.reduceOption (none :: l) = List.reduceOption l
@[simp]
theorem
List.reduceOption_map
{α : Type u_1}
{β : Type u_2}
{l : List (Option α)}
{f : α → β}
:
List.reduceOption (List.map (Option.map f) l) = List.map f (List.reduceOption l)
theorem
List.reduceOption_append
{α : Type u_1}
(l : List (Option α))
(l' : List (Option α))
:
List.reduceOption (l ++ l') = List.reduceOption l ++ List.reduceOption l'
theorem
List.reduceOption_length_eq_iff
{α : Type u_1}
{l : List (Option α)}
:
List.length (List.reduceOption l) = List.length l ↔ ∀ (x : Option α), x ∈ l → Option.isSome x = true
theorem
List.reduceOption_length_lt_iff
{α : Type u_1}
{l : List (Option α)}
:
List.length (List.reduceOption l) < List.length l ↔ none ∈ l
theorem
List.reduceOption_singleton
{α : Type u_1}
(x : Option α)
:
List.reduceOption [x] = Option.toList x
theorem
List.reduceOption_concat_of_some
{α : Type u_1}
(l : List (Option α))
(x : α)
:
List.reduceOption (List.concat l (some x)) = List.concat (List.reduceOption l) x
theorem
List.reduceOption_mem_iff
{α : Type u_1}
{l : List (Option α)}
{x : α}
:
x ∈ List.reduceOption l ↔ some x ∈ l