Often when writing proofs, I'll define a function $f$ pointwise
For example, given a set $A = \{a, b, c\}$ and a set $B = \{1, 2, 3\}$, I might define a function $f:A\rightarrow B$ as follows:
$f(a) = 1$
$f(b) = 2$
$f(c) = 3$
Now let's say in my proof I need to use some property of $f^{-1}$
Clearly $f^{-1}$ exists. But I get hung up on the language around introducing it.
I guess I see my options for the structure of my proof as:
<Introduce/define f pointwise>.Now we define $f^{-1}$
But we can't actually define $f^{-1}$ because function inverses are unique in general, so this is wrong.
In practice this is what I usually do is:
<Introduce/define f pointwise>. Now, given<property I need>of $f^{-1}$,<move on with my proof/life>
But this also makes me uneasy -- so far I've only explicitly defined two sets, $A$ and $B$, and a function $f$ from $A$ to $B$.
In other words, assuming it exists, is $f^{-1}$ an essential property of $f$ that is implied to be present in the universe of objects accessible to my proof (is it "in scope" within my proof, to use computer science terminology) from the moment I define $f$?
What is the correct language to use here when introducing $f^{-1}$ (when its existence has already been established)?