English
Let e be an open partial homeomorphism X ⇒ Y. For nonempty opens U ⊆ X and V with U ≤ V, the inverse restriction on V, followed by inclusion from U to V, equals the inverse restriction on U on the corresponding target.
Русский
Пусть e — открытое частичное гомеоморфизм X ⇒ Y. Для ненулевых открытых U ⊆ X и V с U ≤ V, обратное ограничение на V, затем включение из U в V, равно ограничению на U на соответствующей мишени.
LaTeX
$$$\\mathrm{EqOn}\\bigl(e.subtypeRestr(hV).symm,\\;\\mathrm{Set.inclusion}(hUV) \\circ (e.subtypeRestr(hU)).symm,\\;(e.subtypeRestr(hU)).target\\bigr)$$$
Lean4
theorem subtypeRestr_symm_eqOn_of_le {U V : Opens X} (hU : Nonempty U) (hV : Nonempty V) (hUV : U ≤ V) :
EqOn (e.subtypeRestr hV).symm (Set.inclusion hUV ∘ (e.subtypeRestr hU).symm) (e.subtypeRestr hU).target :=
by
set i := Set.inclusion hUV
intro y hy
dsimp [OpenPartialHomeomorph.subtypeRestr_def] at hy ⊢
have hyV : e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target :=
by
rw [Opens.openPartialHomeomorphSubtypeCoe_target] at hy ⊢
exact hUV hy.2
refine (V.openPartialHomeomorphSubtypeCoe hV).injOn ?_ trivial ?_
· rw [← OpenPartialHomeomorph.symm_target]
apply OpenPartialHomeomorph.map_source
rw [OpenPartialHomeomorph.symm_source]
exact hyV
· rw [(V.openPartialHomeomorphSubtypeCoe hV).right_inv hyV]
change _ = U.openPartialHomeomorphSubtypeCoe hU _
rw [(U.openPartialHomeomorphSubtypeCoe hU).right_inv hy.2]
