Open quotient maps

An open quotient map π : X → Y commutes with taking frontiers of saturated sets: if A is the full preimage of its image, the frontier of π '' A is the image of the frontier of A. This is what lets a decomposition of X into pieces meeting along their frontiers descend to a quotient.

Every homeomorphism is an open quotient map (IsHomeomorph.isOpenQuotientMap).

theorem IsOpenQuotientMap.frontier_image_of_preimage_image_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {π : X → Y} (hπ : IsOpenQuotientMap π) {A : Set X} (hA : π ⁻¹' π '' A = A) : frontier (π '' A) = π '' frontier A

The frontier of the image of a saturated set under an open quotient map is the image of its frontier.

theorem IsHomeomorph.isOpenQuotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {π : X → Y} (hπ : IsHomeomorph π) : IsOpenQuotientMap π

A homeomorphism is an open quotient map.