English
If the composition g ∘ f is proper, and f is surjective, then g is proper.
Русский
Если произведение g ∘ f является правильным и f сюръективна, то g проперна.
LaTeX
$$$Continuous f \land Continuous g \land IsProperMap (g \circ f) \land f \text{ is surjective} \Rightarrow IsProperMap g$$$
Lean4
/-- If the composition of two continuous functions `g ∘ f` is proper and `f` is surjective,
then `g` is proper. -/
theorem isProperMap_of_comp_of_surj (hf : Continuous f) (hg : Continuous g) (hgf : IsProperMap (g ∘ f))
(f_surj : f.Surjective) : IsProperMap g :=
by
refine ⟨hg, fun ℱ z h ↦ ?_⟩
rw [← ℱ.map_comap_of_surjective f_surj, ← mapClusterPt_comp] at h
rcases hgf.clusterPt_of_mapClusterPt h with ⟨x, rfl, hx⟩
rw [← ℱ.map_comap_of_surjective f_surj]
exact ⟨f x, rfl, hx.map hf.continuousAt tendsto_map⟩
