Documentation

Mathlib.Data.List.ReduceOption

Properties of List.reduceOption #

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

source
@[simp]
theorem List.reduceOption_cons_of_some {α : Type u_1} (x : α) (l : List (Option α)) :
(some x :: l).reduceOption = x :: l.reduceOption
source
@[simp]
theorem List.reduceOption_cons_of_none {α : Type u_1} (l : List (Option α)) :
(none :: l).reduceOption = l.reduceOption
source
@[simp]
theorem List.reduceOption_nil {α : Type u_1} :
[].reduceOption = []
source
@[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
source
theorem List.reduceOption_append {α : Type u_1} (l l' : List (Option α)) :
(l ++ l').reduceOption = l.reduceOption ++ l'.reduceOption
source
theorem List.reduceOption_length_eq {α : Type u_1} {l : List (Option α)} :
l.reduceOption.length = (List.filter Option.isSome l).length
source
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
source
theorem List.reduceOption_length_le {α : Type u_1} (l : List (Option α)) :
l.reduceOption.length ≤ l.length
source
theorem List.reduceOption_length_eq_iff {α : Type u_1} {l : List (Option α)} :
l.reduceOption.length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true
source
theorem List.reduceOption_length_lt_iff {α : Type u_1} {l : List (Option α)} :
l.reduceOption.length < l.length ↔ none ∈ l
source
theorem List.reduceOption_singleton {α : Type u_1} (x : Option α) :
[x].reduceOption = x.toList
source
theorem List.reduceOption_concat {α : Type u_1} (l : List (Option α)) (x : Option α) :
(l.concat x).reduceOption = l.reduceOption ++ x.toList
source
theorem List.reduceOption_concat_of_some {α : Type u_1} (l : List (Option α)) (x : α) :
(l.concat (some x)).reduceOption = l.reduceOption.concat x
source
theorem List.reduceOption_mem_iff {α : Type u_1} {l : List (Option α)} {x : α} :
x ∈ l.reduceOption ↔ some x ∈ l
source
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