English
If g∘f is locally a homeomorph on s and f is locally a homeomorph on s, then g is locally a homeomorph on f'' s.
Русский
Если g∘f локально гомеоморфизм на s и f локально гомеоморфизм на s, то g локально гомеоморфизм на f'' s.
LaTeX
$$$IsLocalHomeomorphOn\\,(g\\circ f)\\, s \\Rightarrow IsLocalHomeomorphOn\\, f\\, s \\Rightarrow IsLocalHomeomorphOn\\, g\\, (f'' s)$$$
Lean4
theorem of_comp_right (hgf : IsLocalHomeomorphOn (g ∘ f) s) (hf : IsLocalHomeomorphOn f s) :
IsLocalHomeomorphOn g (f '' s) :=
mk g _ <| by
rintro _ ⟨x, hx, rfl⟩
obtain ⟨f, hxf, rfl⟩ := hf x hx
obtain ⟨gf, hgf, he⟩ := hgf x hx
refine ⟨f.symm.trans gf, ⟨f.map_source hxf, ?_⟩, fun y hy ↦ ?_⟩
· apply (f.left_inv hxf).symm ▸ hgf
· change g y = gf (f.symm y)
rw [← he, Function.comp_apply, f.right_inv hy.1]
