Documentation

Mathlib.Topology.Maps.OpenQuotient

Open quotient maps #

An open quotient map is an open map f : X → Y which is both an open map and a quotient map. Equivalently, it is a surjective continuous open map. We use the latter characterization as a definition.

Many important quotient maps are open quotient maps, including

Contrary to general quotient maps, the category of open quotient maps is closed under Prod.map.

An open quotient map is a quotient map.

@[deprecated IsOpenQuotientMap.isQuotientMap]
theorem IsOpenQuotientMap.quotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (h : IsOpenQuotientMap f) :

Alias of IsOpenQuotientMap.isQuotientMap.


An open quotient map is a quotient map.

@[deprecated IsOpenQuotientMap.iff_isOpenMap_isQuotientMap]

Alias of IsOpenQuotientMap.iff_isOpenMap_isQuotientMap.

@[deprecated IsOpenQuotientMap.of_isOpenMap_isQuotientMap]

Alias of IsOpenQuotientMap.of_isOpenMap_isQuotientMap.

theorem IsOpenQuotientMap.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XY} {g : YZ} (hg : IsOpenQuotientMap g) (hf : IsOpenQuotientMap f) :
theorem IsOpenQuotientMap.map_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (h : IsOpenQuotientMap f) (x : X) :
Filter.map f (nhds x) = nhds (f x)
theorem IsOpenQuotientMap.continuous_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XY} (h : IsOpenQuotientMap f) {g : YZ} :
theorem IsOpenQuotientMap.continuousAt_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XY} (h : IsOpenQuotientMap f) {g : YZ} {x : X} :
theorem IsOpenQuotientMap.dense_preimage_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (h : IsOpenQuotientMap f) {s : Set Y} :