English
Let e be an Open Partial Homeomorphism from X to Y. Then its inverse map e^{-1} is given by e.symm, and it serves as the inverse on the respective source/target. In particular, for every y in e.target, e.symm(y) ∈ e.source and e(e.symm(y)) = y; and for every x in e.source, e.symm(e(x)) = x.
Русский
Пусть e — открыто-частичный гомеоморфизм X → Y. Тогда обратная к нему карта e^{-1} задаётся как e.symm и является обратной на соответствующих областях. В частности, для каждого y ∈ e.target выполняется e.symm(y) ∈ e.source и e(e.symm(y)) = y; и для каждого x ∈ e.source выполняется e.symm(e(x)) = x.
LaTeX
$$$\forall y \in e.target:\ e( e.symm(y) ) = y \quad\text{и}\quad \forall x \in e.source:\ e.symm(e(x)) = x.$$$
Lean4
/-- See Note [custom simps projection] -/
def symm_apply (e : OpenPartialHomeomorph X Y) : Y → X :=
e.symm
