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

• IsQuasiSeparated: 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.
• QuasiSeparatedSpace: A topological space is quasi-separated if the intersections of any pairs of compact open subsets are still compact.
• QuasiSeparatedSpace.of_openEmbedding: If f : α → β is an open embedding, and β is a quasi-separated space, then so is α.

def IsQuasiSeparated {α : Type u_1} [TopologicalSpace α] (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 QuasiSeparatedSpace only when s is open.

Equations

• IsQuasiSeparated s = ∀ (U V : Set α), U ⊆ s → IsOpen U → IsCompact U → V ⊆ s → IsOpen V → IsCompact V → IsCompact (U ∩ V)

theorem quasiSeparatedSpace_iff (α : Type u_3) [TopologicalSpace α] : QuasiSeparatedSpace α ↔ ∀ (U V : Set α), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

class QuasiSeparatedSpace (α : Type u_3) [TopologicalSpace α] : Prop

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

• inter_isCompact : ∀ (U V : Set α), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

  The intersection of two open compact subsets of a quasi-separated space is compact.

theorem isQuasiSeparated_univ_iff {α : Type u_3} [TopologicalSpace α] : IsQuasiSeparated Set.univ ↔ QuasiSeparatedSpace α

theorem isQuasiSeparated_univ {α : Type u_3} [TopologicalSpace α] [QuasiSeparatedSpace α] : IsQuasiSeparated Set.univ

theorem IsQuasiSeparated.image_of_embedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (H : IsQuasiSeparated s) (h : Embedding f) : IsQuasiSeparated (f '' s)

theorem OpenEmbedding.isQuasiSeparated_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (h : OpenEmbedding f) {s : Set α} : IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s)

theorem isQuasiSeparated_iff_quasiSeparatedSpace {α : Type u_1} [TopologicalSpace α] (s : Set α) (hs : IsOpen s) : IsQuasiSeparated s ↔ QuasiSeparatedSpace ↑s

theorem IsQuasiSeparated.of_subset {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} (ht : IsQuasiSeparated t) (h : s ⊆ t) : IsQuasiSeparated s

instance T2Space.to_quasiSeparatedSpace {α : Type u_1} [TopologicalSpace α] [T2Space α] : QuasiSeparatedSpace α

Equations

• (_ : QuasiSeparatedSpace α) = (_ : QuasiSeparatedSpace α)

instance NoetherianSpace.to_quasiSeparatedSpace {α : Type u_1} [TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] : QuasiSeparatedSpace α

Equations

• (_ : QuasiSeparatedSpace α) = (_ : QuasiSeparatedSpace α)

theorem IsQuasiSeparated.of_quasiSeparatedSpace {α : Type u_1} [TopologicalSpace α] (s : Set α) [QuasiSeparatedSpace α] : IsQuasiSeparated s

theorem QuasiSeparatedSpace.of_openEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (h : OpenEmbedding f) [QuasiSeparatedSpace β] : QuasiSeparatedSpace α