English
Let e be an open partial homeomorphism between spaces X and Y, and let U be a nonempty open subset of X. Then the inverse relation of e, restricted to U, coincides on the target with the map obtained by composing Subtype.val with the inverse of the restricted e to U.
Русский
Пусть e — открытое частичное гомеоморфизм между пространствами X и Y, и U— ненулевое открытое подмножество X. Тогда обратная карта e, ограниченная на U, совпадает на целевом множестве с отображением Subtype.val ∘ (e.subtypeRestr hU)^{-1}.
LaTeX
$$$\\mathrm{EqOn}\\bigl(e.{\\mathrm{symm}},\\mathrm{Subtype.val} \\circ (e.subtypeRestr(hU)).symm, (e.subtypeRestr(hU)).target\\bigr)$$$
Lean4
theorem subtypeRestr_symm_eqOn {U : Opens X} (hU : Nonempty U) :
EqOn e.symm (Subtype.val ∘ (e.subtypeRestr hU).symm) (e.subtypeRestr hU).target :=
by
intro y hy
rw [eq_comm, eq_symm_apply _ _ hy.1]
· change restrict _ e _ = _
rw [← subtypeRestr_coe _ hU, (e.subtypeRestr hU).right_inv hy]
· have := map_target _ hy; rwa [subtypeRestr_source] at this
