# Quasi-separated spaces #

A topological space is quasi-separated if the intersections of any pairs of compact open subsets are still compact. Notable examples include spectral spaces, Noetherian spaces, and Hausdorff spaces.

A non-example is the interval [0, 1] with doubled origin: the two copies of [0, 1] are compact open subsets, but their intersection (0, 1] is not.

## Main results #

• IsQuasiSeparated: A subset s of a topological space is quasi-separated if the intersections of any pairs of compact open subsets of s are still compact.
• QuasiSeparatedSpace: A topological space is quasi-separated if the intersections of any pairs of compact open subsets are still compact.
• QuasiSeparatedSpace.of_openEmbedding: If f : α → β is an open embedding, and β is a quasi-separated space, then so is α.
def IsQuasiSeparated {α : Type u_1} [] (s : Set α) :

A subset s of a topological space is quasi-separated if the intersections of any pairs of compact open subsets of s are still compact.

Note that this is equivalent to s being a QuasiSeparatedSpace only when s is open.

Equations
Instances For
theorem quasiSeparatedSpace_iff (α : Type u_3) [] :
∀ (U V : Set α), IsCompact (U V)
class QuasiSeparatedSpace (α : Type u_3) [] :

A topological space is quasi-separated if the intersections of any pairs of compact open subsets are still compact.

• inter_isCompact : ∀ (U V : Set α), IsCompact (U V)

The intersection of two open compact subsets of a quasi-separated space is compact.

Instances
theorem isQuasiSeparated_univ_iff {α : Type u_3} [] :
theorem isQuasiSeparated_univ {α : Type u_3} [] :
theorem IsQuasiSeparated.image_of_embedding {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (H : ) (h : ) :
theorem OpenEmbedding.isQuasiSeparated_iff {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (h : ) {s : Set α} :
theorem isQuasiSeparated_iff_quasiSeparatedSpace {α : Type u_1} [] (s : Set α) (hs : ) :
theorem IsQuasiSeparated.of_subset {α : Type u_1} [] {s : Set α} {t : Set α} (ht : ) (h : s t) :
instance T2Space.to_quasiSeparatedSpace {α : Type u_1} [] [] :
Equations
• =
Equations
• =
theorem IsQuasiSeparated.of_quasiSeparatedSpace {α : Type u_1} [] (s : Set α) :
theorem QuasiSeparatedSpace.of_openEmbedding {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (h : ) :