mathlib3 documentation

topology.quasi_separated

Quasi-separated spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

def is_quasi_separated {α : Type u_1} [topological_space α] (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
@[class]
structure quasi_separated_space (α : Type u_3) [topological_space α] :
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.image_of_embedding {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} (H : is_quasi_separated s) (h : embedding f) :
theorem is_quasi_separated.of_subset {α : Type u_1} [topological_space α] {s t : set α} (ht : is_quasi_separated t) (h : s t) :
@[protected, instance]