English
Let e, e' be open partial homeomorphisms X ⟶ Z. For any hf that makes f an open embedding X ⟶ X', the lifted maps satisfy the equality (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) = e.symm.trans e'.
Русский
Пусть e, e' — открытые частичные гомоморфизмы X ⟶ Z. При любом hf, делающем f: X ⟶ X' открытым вложением, полученные поднятые отображения удовлетворяют равенству (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) = e.symm.trans e'.
LaTeX
$$$ (e \\,.lift\\_openEmbedding\\,(hf)).\\text{symm}.\\text{trans} (e'.\\lift\\_openEmbedding\\,(hf)) = e.\\text{symm}.\\text{trans} e' $$$
Lean4
@[simp, mfld_simps]
theorem lift_openEmbedding_trans (e e' : OpenPartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
(e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) = e.symm.trans e' :=
by
ext z
· exact e.lift_openEmbedding_trans_apply e' hf z
· simp [hf.injective.extend_apply e]
· simp_rw [OpenPartialHomeomorph.trans_source, e.lift_openEmbedding_symm_source, e.symm_source,
e.lift_openEmbedding_symm, e'.lift_openEmbedding_source]
refine ⟨fun ⟨hx, ⟨y, hy, hxy⟩⟩ ↦ ⟨hx, ?_⟩, fun ⟨hx, hx'⟩ ↦ ⟨hx, mem_image_of_mem f hx'⟩⟩
rw [mem_preimage]; rw [comp_apply] at hxy
exact (hf.injective hxy) ▸ hy
