mathlib documentation

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 #

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
theorem quasi_separated_space_iff (α : Type u_3) [topological_space α] :
quasi_separated_space α ∀ (U V : set α), is_open Uis_compact Uis_open Vis_compact Vis_compact (U V)
@[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 open_embedding.is_quasi_separated_iff {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (h : open_embedding f) {s : set α} :
theorem is_quasi_separated.of_subset {α : Type u_1} [topological_space α] {s t : set α} (ht : is_quasi_separated t) (h : s t) :
@[protected, instance]
theorem quasi_separated_space.of_open_embedding {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (h : open_embedding f) [quasi_separated_space β] :