Lean4
/-- Extend an open partial homeomorphism `e : X → Z` to `X' → Z`, using an open embedding
`ι : X → X'`. On `ι(X)`, the extension is specified by `e`; its value elsewhere is arbitrary
(and uninteresting). -/
noncomputable def lift_openEmbedding (e : OpenPartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
OpenPartialHomeomorph X' Z
where
toFun := extend f e (fun _ ↦ (Classical.arbitrary Z))
invFun := f ∘ e.invFun
source := f '' e.source
target := e.target
map_source' := by
rintro x ⟨x₀, hx₀, hxx₀⟩
rw [← hxx₀, hf.injective.extend_apply e]
exact e.map_source' hx₀
map_target' z hz := mem_image_of_mem f (e.map_target' hz)
left_inv' := by
intro x ⟨x₀, hx₀, hxx₀⟩
rw [← hxx₀, hf.injective.extend_apply e, comp_apply]
congr
exact e.left_inv' hx₀
right_inv' z hz := by simpa only [comp_apply, hf.injective.extend_apply e] using e.right_inv' hz
open_source := hf.isOpenMap _ e.open_source
open_target := e.open_target
continuousOn_toFun := by
by_cases Nonempty X; swap
· intro x hx; simp_all
set F := (extend f e (fun _ ↦ (Classical.arbitrary Z))) with F_eq
have heq : EqOn F (e ∘ (hf.toOpenPartialHomeomorph).symm) (f '' e.source) :=
by
intro x ⟨x₀, hx₀, hxx₀⟩
rw [← hxx₀, F_eq, hf.injective.extend_apply e, comp_apply, hf.toOpenPartialHomeomorph_left_inv]
have : ContinuousOn (e ∘ (hf.toOpenPartialHomeomorph).symm) (f '' e.source) :=
by
apply e.continuousOn_toFun.comp; swap
· intro x' ⟨x, hx, hx'x⟩
rw [← hx'x, hf.toOpenPartialHomeomorph_left_inv]; exact hx
have : ContinuousOn (hf.toOpenPartialHomeomorph).symm (f '' univ) :=
(hf.toOpenPartialHomeomorph).continuousOn_invFun
exact this.mono <| image_mono <| subset_univ _
exact ContinuousOn.congr this heq
continuousOn_invFun := hf.continuous.comp_continuousOn e.continuousOn_invFun
