English
If g ∘ f is a local homeomorphism, and g is a local homeomorphism, and f is continuous, then f is a local homeomorphism.
Русский
Если композиция g ∘ f — локальная гомеоморфия, а g — локальная гомеоморфия, и f непрерывна, тогда f — локальная гомеоморфия.
LaTeX
$$$\operatorname{IsLocalHomeomorph}(g \circ f) \Rightarrow \operatorname{IsLocalHomeomorph}(f)\quad\text{given } \operatorname{IsLocalHomeomorph}(g) \text{ and } \text{Continuous}(f)$$$
Lean4
theorem of_comp (hgf : IsLocalHomeomorph (g ∘ f)) (hg : IsLocalHomeomorph g) (cont : Continuous f) :
IsLocalHomeomorph f :=
isLocalHomeomorph_iff_isLocalHomeomorphOn_univ.mpr <|
hgf.isLocalHomeomorphOn.of_comp_left hg.isLocalHomeomorphOn fun _ _ ↦ cont.continuousAt
