English
Two open partial homeomorphisms are equal if their forward maps, inverse maps and source agree.
Русский
Два открытых частичных гомеоморфа равны, если совпадают их отображения вперёд, обратные отображения и источник.
LaTeX
$$$e = e' \iff (\forall x, e(x)=e'(x)) \land (\forall x, e^{-1}(x)=e'^{-1}(x)) \land (e.source = e'.source)$$$
Lean4
/-- Two open partial homeomorphisms are equal when they have equal `toFun`, `invFun` and `source`.
It is not sufficient to have equal `toFun` and `source`, as this only determines `invFun` on
the target. This would only be true for a weaker notion of equality, arguably the right one,
called `EqOnSource`. -/
@[ext]
protected theorem ext (e' : OpenPartialHomeomorph X Y) (h : ∀ x, e x = e' x) (hinv : ∀ x, e.symm x = e'.symm x)
(hs : e.source = e'.source) : e = e' :=
toPartialEquiv_injective (PartialEquiv.ext h hinv hs)
