English
Two equivalent open partial homeomorphisms are equal when restricted to their source’s interiors, provided their sources agree on the interior.
Русский
Два эквивалентных открытых частичных гомеоморфизма равны при ограничении их наInterior источников, если Interiors совпадают.
LaTeX
$$$ (e.source \cap interior s) = (e'.source \cap interior s) \Rightarrow e.restr s \approx e'.restr s $$$
Lean4
theorem restr_symm_trans {e' : OpenPartialHomeomorph X Y} (hs : IsOpen s) (hs' : IsOpen (e '' s))
(hs'' : s ⊆ e.source) : (e.restr s).symm.trans e' ≈ (e.symm.trans e').restr (e '' s) :=
by
refine ⟨?_, ?_⟩
· simp only [trans_toPartialEquiv, symm_toPartialEquiv, restr_toPartialEquiv, PartialEquiv.trans_source,
PartialEquiv.symm_source, PartialEquiv.restr_target, coe_coe_symm, PartialEquiv.restr_coe_symm,
PartialEquiv.restr_source]
rw [interior_eq_iff_isOpen.mpr hs', interior_eq_iff_isOpen.mpr hs]
-- Get rid of the middle term, which is merely distracting.
rw [inter_assoc, inter_assoc, inter_comm _ (e '' s), ← inter_assoc, ← inter_assoc]
congr 1
-- Now, just a bunch of rewrites: should this be a separate lemma?
rw [← image_source_inter_eq', ← image_source_eq_target]
refine image_inter_on ?_
intro x hx y hy h
rw [← left_inv e hy, ← left_inv e (hs'' hx), h]
· simp_rw [coe_trans, restr_symm_apply, restr_apply, coe_trans]
intro x hx
simp
