# mathlibdocumentation

topology.quasi_separated

# 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 #

• is_quasi_separated: 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.
• quasi_separated_space: A topological space is quasi-separated if the intersections of any pairs of compact open subsets are still compact.
• quasi_separated_space.of_open_embedding: If f : α → β is an open embedding, and β is a quasi-separated space, then so is α.
def is_quasi_separated {α : Type u_1} (s : set α) :
Prop

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 quasi_separated_space only when s is open.

Equations
theorem quasi_separated_space_iff (α : Type u_3)  :
∀ (U V : set α), is_compact (U V)
@[class]
structure quasi_separated_space (α : Type u_3)  :
Prop

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

Instances of this typeclass
theorem is_quasi_separated_univ_iff {α : Type u_1}  :
theorem is_quasi_separated_univ {α : Type u_1}  :
theorem is_quasi_separated.image_of_embedding {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (H : is_quasi_separated s) (h : embedding f) :
theorem open_embedding.is_quasi_separated_iff {α : Type u_1} {β : Type u_2} {f : α → β} (h : open_embedding f) {s : set α} :
theorem is_quasi_separated_iff_quasi_separated_space {α : Type u_1} (s : set α) (hs : is_open s) :
theorem is_quasi_separated.of_subset {α : Type u_1} {s t : set α} (ht : is_quasi_separated t) (h : s t) :
@[protected, instance]
def t2_space.to_quasi_separated_space {α : Type u_1} [t2_space α] :
@[protected, instance]
theorem is_quasi_separated.of_quasi_separated_space {α : Type u_1} (s : set α)  :
theorem quasi_separated_space.of_open_embedding {α : Type u_1} {β : Type u_2} {f : α → β} (h : open_embedding f)  :