Library
▹
Essentials
▹
Functions
Definition 1.5.3.
Let
X
,
Y
be sets,
f
:
X
→
Y
be a
function
,
S
⊆
X
. We define:
f
(
S
)
:
=
{
f
(
x
)
:
x
∈
S
}
References.
https://en.wikipedia.org/wiki/Image_(mathematics)
https://proofwiki.org/wiki/Definition:Image_(Set_Theory)/Mapping/Subset
https://leanprover-community.github.io/mathlib_docs/init/data/set.html#set.image