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
@[simp]
theorem List.reduceOption_replicate_none {α : Type u_1} {n : ℕ} :
(List.replicate n none).reduceOption = []
source
theorem List.reduceOption_eq_nil_iff {α : Type u_1} (l : List (Option α)) :
l.reduceOption = [] ↔ ∃ (n : ℕ), l = List.replicate n none
source
theorem List.reduceOption_eq_singleton_iff {α : Type u_1} (l : List (Option α)) (a : α) :
l.reduceOption = [a] ↔ ∃ (m : ℕ), ∃ (n : ℕ), l = List.replicate m none ++ some a :: List.replicate n none
source
theorem List.reduceOption_eq_append_iff {α : Type u_1} (l : List (Option α)) (l'₁ l'₂ : List α) :
l.reduceOption = l'₁ ++ l'₂ ↔ ∃ (l₁ : List (Option α)), ∃ (l₂ : List (Option α)), l = l₁ ++ l₂ ∧ l₁.reduceOption = l'₁ ∧ l₂.reduceOption = l'₂
source
theorem List.reduceOption_eq_concat_iff {α : Type u_1} (l : List (Option α)) (l' : List α) (a : α) :
l.reduceOption = l'.concat a ↔ ∃ (l₁ : List (Option α)), ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ 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