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 #

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 α.

source

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

is_quasi_separated s = ∀ (U V : set α), U ⊆ s → is_open U → is_compact U → V ⊆ s → is_open V → is_compact V → is_compact (U ∩ V)

source

theorem quasi_separated_space_iff (α : Type u_3) [topological_space α] :

quasi_separated_space α ↔ ∀ (U V : set α), is_open U → is_compact U → is_open V → is_compact V → is_compact (U ∩ V)

source

@[class]

structure quasi_separated_space (α : Type u_3) [topological_space α] :

Prop

inter_is_compact : ∀ (U V : set α), is_open U → is_compact U → is_open V → is_compact V → is_compact (U ∩ V)

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

Instances of this typeclass

source

theorem is_quasi_separated_univ_iff {α : Type u_1} [topological_space α] :

is_quasi_separated set.univ ↔ quasi_separated_space α

source

theorem is_quasi_separated_univ {α : Type u_1} [topological_space α] [quasi_separated_space α] :

is_quasi_separated set.univ

source

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) :

is_quasi_separated (f '' s)

source

theorem open_embedding.is_quasi_separated_iff {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (h : open_embedding f) {s : set α} :

is_quasi_separated s ↔ is_quasi_separated (f '' s)

source

theorem is_quasi_separated_iff_quasi_separated_space {α : Type u_1} [topological_space α] (s : set α) (hs : is_open s) :

is_quasi_separated s ↔ quasi_separated_space ↥s

source

theorem is_quasi_separated.of_subset {α : Type u_1} [topological_space α] {s t : set α} (ht : is_quasi_separated t) (h : s ⊆ t) :

is_quasi_separated s

source

@[protected, instance]

def t2_space.to_quasi_separated_space {α : Type u_1} [topological_space α] [t2_space α] :

quasi_separated_space α

source

@[protected, instance]

def noetherian_space.to_quasi_separated_space {α : Type u_1} [topological_space α] [topological_space.noetherian_space α] :

quasi_separated_space α

source

theorem is_quasi_separated.of_quasi_separated_space {α : Type u_1} [topological_space α] (s : set α) [quasi_separated_space α] :

is_quasi_separated s

source

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 β] :

quasi_separated_space α