Documentation
Init
.
Data
.
Option
.
Function
Search
return to top
source
Imports
Init.Data.Function
Init.Data.Option.Lemmas
Imported by
Option
.
map_injective
source
theorem
Option
.
map_injective
{
α
:
Type
u_1}
{
β
:
Type
u_2}
{
f
:
α
→
β
}
(
hf
:
Function.Injective
f
)
:
Function.Injective
(
Option.map
f
)