of_comp_surjective — Mathlib

English

If f is surjective, continuous, and g ∘ f is a closed map, then g is a closed map.

Русский

Если f сюръективно непрерывно, и если г ∘ f — замкнутое отображение, то g — замкнутое отображение.

LaTeX

$$$\\text{Surjective}(f)\\land\\text{Continuous}(f)\\land IsClosedMap(g\\circ f) \\Rightarrow IsClosedMap(g)$$$

Lean4

protected theorem of_comp_surjective (hf : Surjective f) (hf' : Continuous f) (hfg : IsClosedMap (g ∘ f)) :
    IsClosedMap g := by
  intro K hK
  rw [← image_preimage_eq K hf, ← image_comp]
  exact hfg _ (hK.preimage hf')

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