isQuotientMap — Mathlib

English

If f is open, continuous, and surjective, then f is a quotient map.

Русский

Если f открытое, непрерывное и сюръективное отображение, тогда f является квартообразующим (квационным) отображением.

LaTeX

$$$$IsOpenMap(f) \\land Continuous(f) \\land Surjective(f) \\rightarrow IsQuotientMap(f)$$$$

Lean4

/-- A continuous surjective open map is a quotient map. -/
theorem isQuotientMap (open_map : IsOpenMap f) (cont : Continuous f) (surj : Surjective f) : IsQuotientMap f :=
  isQuotientMap_iff.2 ⟨surj, fun s => ⟨fun h => h.preimage cont, fun h => surj.image_preimage s ▸ open_map _ h⟩⟩

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