Documentation
Mathlib
.
Data
.
List
.
ReduceOption
Search
return to top
source
Imports
Init
Mathlib.Data.List.Basic
Imported by
List
.
reduceOption_cons_of_some
List
.
reduceOption_cons_of_none
List
.
reduceOption_nil
List
.
reduceOption_map
List
.
reduceOption_append
List
.
reduceOption_replicate_none
List
.
reduceOption_eq_nil_iff
List
.
reduceOption_eq_singleton_iff
List
.
reduceOption_eq_append_iff
List
.
reduceOption_eq_concat_iff
List
.
reduceOption_length_eq
List
.
length_eq_reduceOption_length_add_filter_none
List
.
reduceOption_length_le
List
.
reduceOption_length_eq_iff
List
.
reduceOption_length_lt_iff
List
.
reduceOption_singleton
List
.
reduceOption_concat
List
.
reduceOption_concat_of_some
List
.
reduceOption_mem_iff
List
.
reduceOption_get?_iff
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 :
α
→
β
}
:
(
map
(
Option.map
f
)
l
)
.
reduceOption
=
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 :
ℕ
}
:
(
replicate
n
none
)
.
reduceOption
=
[
]
source
theorem
List
.
reduceOption_eq_nil_iff
{α :
Type
u_1}
(l :
List
(
Option
α
)
)
:
l
.
reduceOption
=
[
]
↔
∃
(
n
:
ℕ
)
,
l
=
replicate
n
none
source
theorem
List
.
reduceOption_eq_singleton_iff
{α :
Type
u_1}
(l :
List
(
Option
α
)
)
(a :
α
)
:
l
.
reduceOption
=
[
a
]
↔
∃
(
m
:
ℕ
)
,
∃
(
n
:
ℕ
)
,
l
=
replicate
m
none
++
some
a
::
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
=
(
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
+
(
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