Does this formula for the derivative of a differentiable inverse have a name?

28 Views Asked by At

Consider the following lemma:

Let $f:X \to Y$ be an invertible function, with inverse $f^{-1}:Y \to X$,and let $f(x_0) = y_0$. If $f$ is differentiable at $x_0$ and $f^{-1}$ is differentiable at $y_0$, then $$(f^{-1})'(y_0) = \frac{1}{f'(x_0)}.$$

This is introduced before the inverse function theorem in Tao's Analysis I, as a sort of precursor to the actual result. I am wondering if this lemma has a name, or if anyone has a good suggestion for a descriptive name to give it, just for my own personal notes.