Documentation
Mathlib
.
Init
.
Data
.
List
.
Instances
Search
Google site search
Mathlib
.
Init
.
Data
.
List
.
Instances
source
Imports
Init
Mathlib.Init.Data.List.Lemmas
Imported by
List
.
bind_singleton
List
.
bind_singleton'
List
.
map_eq_bind
List
.
bind_assoc
List
.
instMonad
List
.
instLawfulMonad
List
.
instAlternative
List
.
decidableBex
List
.
decidableBall
Decidable Instances for
List
not (yet) in
Std
source
theorem
List
.
bind_singleton
{α :
Type
u}
{β :
Type
v}
(f :
α
→
List
β
)
(x :
α
)
:
List.bind
[
x
]
f
=
f
x
source
@[simp]
theorem
List
.
bind_singleton'
{α :
Type
u}
(l :
List
α
)
:
(
List.bind
l
fun
x
=>
[
x
]
)
=
l
source
theorem
List
.
map_eq_bind
{α :
Type
u_1}
{β :
Type
u_2}
(f :
α
→
β
)
(l :
List
α
)
:
List.map
f
l
=
List.bind
l
fun
x
=>
[
f
x
]
source
theorem
List
.
bind_assoc
{γ :
Type
w}
{α :
Type
u_1}
{β :
Type
u_2}
(l :
List
α
)
(f :
α
→
List
β
)
(g :
β
→
List
γ
)
:
List.bind
(
List.bind
l
f
)
g
=
List.bind
l
fun
x
=>
List.bind
(
f
x
)
g
source
instance
List
.
instMonad
:
Monad
List
source
instance
List
.
instLawfulMonad
:
LawfulMonad
List
source
instance
List
.
instAlternative
:
Alternative
List
source
instance
List
.
decidableBex
{α :
Type
u}
{p :
α
→
Prop
}
[
DecidablePred
p
]
(l :
List
α
)
:
Decidable
(
∃
x
,
x
∈
l
∧
p
x
)
Equations
One or more equations did not get rendered due to their size.
List.decidableBex
[]
=
isFalse
(_ :
¬
∃
x
,
x
∈
[]
∧
p
x
)
source
instance
List
.
decidableBall
{α :
Type
u}
{p :
α
→
Prop
}
[
DecidablePred
p
]
(l :
List
α
)
:
Decidable
(
(
x
:
α
) →
x
∈
l
→
p
x
)