I recently carried out a proof that required some tedious notation, so I was hoping the S.E. community could offer some input on how I could "make my life easier".
Specifically, the proof leads with the following definition of a function $f$:
$f: A \overset{1-1}\longrightarrow B$
The other relevant information is as follows:
$B \subseteq A$
Informally, we define the function $f^n: A \rightarrow A$ by iterating $f$ $n$ times. $f^0$ is the identify function $I_A$.
$H_n=f^n[A]\setminus f^n[B]$
The aim of the proof was to demonstrate that, "...$f$ maps $H_n$ bijectively onto $H_{n+1}$".
The way I attempted to formalize this claim was as follows:
$\forall n \in \omega \big ( f \upharpoonright H_n: H_n \xrightarrow[onto]{1-1} H_{n+1}\big)$, which is a straightforward induction proof...and, as a side note, for any $n$, $H_n \subseteq A$...so $f$ is defined on these sets.
However, when trying to prove the surjectivity (onto) claim, I would write the following statement:
Prove that $f\upharpoonright H_n[H_n]=H_{n+1}$
The even more tediuous way of writing this is if you express $H_n$ and $H_{n+1}$ in its full form to yield the following statement:
Prove $f \upharpoonright f^n[A]\setminus f^n[B] \Big [f^n[A]\setminus f^n[B] \Big]=f^{n+1}[A]\setminus f^{n+1}[B]$
I wondered if there was a cleaner convention to write such statements.
In my book The Foundations of Mathematics by Kenneth Kunen, the following definition is given:
$F[A]=\text{ran}(F\upharpoonright A)$
Using that definition, it would seem as though $f\upharpoonright H_n[H_n]=\text{ran}(f\upharpoonright H_n \upharpoonright H_n)$
The syntax "$f\upharpoonright H_n \upharpoonright H_n$" is a little weird...but I am guessing that this effectively defaults to simply "$f\upharpoonright H_n$".
Therefore, it seems like the following is true:
$f\upharpoonright H_n[H_n]=\text{ran}(f\upharpoonright H_n \upharpoonright H_n)=\text{ran}(f\upharpoonright H_n)=f[H_n]$
So instead of using "$f\upharpoonright H_n[H_n]$", I should instead (for notational convenience) use "$f[H_n]$" and simply remember that whatever I prove is specific to "$f$ when its domain is $H_n$".
Is this the standard convention that I should use? Or is there a better/preferred one?