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 subsets
of a topological space is quasi-separated if the intersections of any pairs of compact open subsets ofs
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
: Iff : α → β
is an open embedding, andβ
is a quasi-separated space, then so isα
.
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)
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)
@[class]
- 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
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)
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)
theorem
is_quasi_separated_iff_quasi_separated_space
{α : Type u_1}
[topological_space α]
(s : set α)
(hs : is_open s) :
theorem
is_quasi_separated.of_subset
{α : Type u_1}
[topological_space α]
{s t : set α}
(ht : is_quasi_separated t)
(h : s ⊆ t) :
@[protected, instance]
@[protected, instance]
def
noetherian_space.to_quasi_separated_space
{α : Type u_1}
[topological_space α]
[topological_space.noetherian_space α] :
theorem
is_quasi_separated.of_quasi_separated_space
{α : Type u_1}
[topological_space α]
(s : set α)
[quasi_separated_space α] :
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 β] :