English
See 208008; the restricted open restriction has its PartialEquiv equal to the restriction of the original.
Русский
См. 208008; ограниченная открытая ограничение имеет свою частичную эквивалентность равной ограничению исходной.
LaTeX
$$$(e.restrOpen s hs).toPartialEquiv = e.toPartialEquiv.restr s$$$
Lean4
/-- Restricting an open partial homeomorphism `e` to `e.source ∩ interior s`. We use the interior to
make sure that the restriction is well defined whatever the set s, since open partial homeomorphisms
are by definition defined on open sets. In applications where `s` is open, this coincides with the
restriction of partial equivalences. -/
@[simps! (attr := mfld_simps) -fullyApplied apply symm_apply, simps! -isSimp source target]
protected def restr (s : Set X) : OpenPartialHomeomorph X Y :=
e.restrOpen (interior s) isOpen_interior
