isProperMap_of_comp_of_t2 — Mathlib

English

If the diagram satisfies h, hf, hp, hq, hg and H, then p is a quotient map.

Русский

Если диаграмма удовлетворяет условиям h, hf, hp, hq, hg и H, тогда p является квотируемым отображением.

LaTeX

$$$\mathrm{IsQuotientMap}(p)$$$

Lean4

/-- If the composition of two continuous functions `f : X → Y` and `g : Y → Z` is proper
and `Y` is T2, then `f` is proper. -/
theorem isProperMap_of_comp_of_t2 [T2Space Y] (hf : Continuous f) (hg : Continuous g) (hgf : IsProperMap (g ∘ f)) :
    IsProperMap f := by
  rw [isProperMap_iff_ultrafilter_of_t2]
  refine ⟨hf, fun 𝒰 y h ↦ ?_⟩
  rw [isProperMap_iff_ultrafilter] at hgf
  rcases hgf.2 ((hg.tendsto y).comp h) with ⟨x, -, hx⟩
  exact ⟨x, hx⟩

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