isOpenQuotientMap_of_surjective — Mathlib

English

If IsInducing f and surjective, then IsOpenQuotientMap f.

Русский

Пусть f индуцирующее и сюръективное, тогда f — открытое факторное отображение.

LaTeX

$$$\mathrm{IsInducing}(f) \rightarrow \mathrm{Function.Surjective}(f) \rightarrow \mathrm{IsOpenQuotientMap}(f)$$$

Lean4

theorem isOpenQuotientMap_of_surjective (ind : IsInducing f) (surj : Function.Surjective f) : IsOpenQuotientMap f
    where
  surjective := surj
  continuous := ind.continuous
  isOpenMap U
    U_open := by
    obtain ⟨V, hV, rfl⟩ := ind.isOpen_iff.mp U_open
    rwa [V.image_preimage_eq surj]

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