Bijection réciproque : définition (MPSI)

Si $f : E \to F$ est bijective, l'application qui à tout $y \in F$ associe son unique antécédent par $f$ est la bijection réciproque de $f$, notée $f^{-1} : F \to E$. Par construction : $$\forall x \in E,\ \forall y \in F,\quad y = f(x) \iff x = f^{-1}(y),$$ $$f^{-1} \circ f = \mathrm{id}_E, \qquad f \circ f^{-1} = \mathrm{id}_F.$$