Documentation
FLT
.
Mathlib
.
Data
.
Set
.
Function
Search
return to top
source
Imports
Init
Mathlib.Data.Set.Function
Imported by
Set
.
codRestrict_range_surjective
source
theorem
Set
.
codRestrict_range_surjective
{
α
:
Type
u_1}
{
ι
:
Type
u_2}
(
f
:
ι
→
α
)
:
Function.Surjective
(
codRestrict
f
(
range
f
)
⋯
)