English
Restriction to e.source ∩ s is equivalent to restriction to s.
Русский
Ограничение до e.source ∩ s эквивалентно ограничению до s.
LaTeX
$$$ e.restr (e.source \cap s) \approx e.restr s $$$
Lean4
theorem symm_trans_restr (e' : OpenPartialHomeomorph X Y) (hs : IsOpen s) :
e'.symm.trans (e.restr s) ≈ (e'.symm.trans e).restr (e'.target ∩ e'.symm ⁻¹' s) :=
by
have ht : IsOpen (e'.target ∩ e'.symm ⁻¹' s) :=
by
rw [← image_source_inter_eq']
exact isOpen_image_source_inter e' hs
refine ⟨?_, ?_⟩
· simp only [trans_toPartialEquiv, symm_toPartialEquiv, restr_toPartialEquiv, PartialEquiv.trans_source,
PartialEquiv.symm_source, coe_coe_symm, PartialEquiv.restr_source, preimage_inter]
-- Shuffle the intersections, pull e'.target into the interior and use interior_inter.
rw [interior_eq_iff_isOpen.mpr hs, ← inter_assoc, inter_comm e'.target, inter_assoc, inter_assoc]
congr 1
nth_rw 2 [← interior_eq_iff_isOpen.mpr e'.open_target]
rw [← interior_inter, ← inter_assoc, inter_self, interior_eq_iff_isOpen.mpr ht]
· simp [Set.eqOn_refl]
