English
If (g ∘ f) is a local homeomorph on s, and g is a local homeomorph on f'' s, with cont on s, then f is a local homeomorph on s.
Русский
Если композиция g∘f локальный гомеоморфизм на s, g локальный гомеоморфизм на f'' s и f непрерывен на s, то f — локальный гомеоморфизм на s.
LaTeX
$$$IsLocalHomeomorphOn\\,(g\\circ f)\\; s \\Rightarrow IsLocalHomeomorphOn\\, f\\, s \\Rightarrow IsLocalHomeomorphOn\\, g\\, (f'' s)$$$
Lean4
theorem of_comp_left (hgf : IsLocalHomeomorphOn (g ∘ f) s) (hg : IsLocalHomeomorphOn g (f '' s))
(cont : ∀ x ∈ s, ContinuousAt f x) : IsLocalHomeomorphOn f s :=
mk f s fun x hx ↦ by
obtain ⟨g, hxg, rfl⟩ := hg (f x) ⟨x, hx, rfl⟩
obtain ⟨gf, hgf, he⟩ := hgf x hx
refine
⟨(gf.restr <| f ⁻¹' g.source).trans g.symm,
⟨⟨hgf, mem_interior_iff_mem_nhds.mpr ((cont x hx).preimage_mem_nhds <| g.open_source.mem_nhds hxg)⟩,
he ▸ g.map_source hxg⟩,
fun y hy ↦ ?_⟩
change f y = g.symm (gf y)
have : f y ∈ g.source := by apply interior_subset hy.1.2
rw [← he, g.eq_symm_apply this (by apply g.map_source this), Function.comp_apply]
