Semi-Inverse Map (半逆写像) (Definition I.1.4)

• Semi-Inverse Map (半逆写像) (Definition I.1.4) #Card
  • 単射の左逆写像。

Back

$f : X \to Y$ が単射のとき、$f^{\sim 1} : f(X) \to X$ を $f^{\sim 1}(f(x)) := x$（$x\in X$）で定める。これを $f$ の半逆写像という。

Lean

Function.invFun f（左逆）。単射なら Function.leftInverse_invFun : LeftInverse (invFun f) f