isProperMap_of_comp_of_inj — Mathlib

English

If the composition g ∘ f is proper and g is injective, then f is proper.

Русский

Если композиция g ∘ f правильна и g инъективна, тогда f правильна.

LaTeX

$$$Continuous f \land Continuous g \land IsProperMap (g \circ f) \land g \text{ injective} \Rightarrow IsProperMap f$$$

Lean4

/-- If the composition of two continuous functions `g ∘ f` is proper and `g` is injective,
then `f` is proper. -/
theorem isProperMap_of_comp_of_inj {f : X → Y} {g : Y → Z} (hf : Continuous f) (hg : Continuous g)
    (hgf : IsProperMap (g ∘ f)) (g_inj : g.Injective) : IsProperMap f :=
  by
  refine ⟨hf, fun ℱ y h ↦ ?_⟩
  rcases hgf.clusterPt_of_mapClusterPt (h.map hg.continuousAt tendsto_map) with ⟨x, hx1, hx2⟩
  exact ⟨x, g_inj hx1, hx2⟩

Похожие утверждения