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_isOpenEmbedding: 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.

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 quasiSeparatedSpace_iff (α : Type u_3) [TopologicalSpace α] : QuasiSeparatedSpace α ↔ ∀ (U V : Set α), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

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_isEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (H : IsQuasiSeparated s) (h : Topology.IsEmbedding f) : IsQuasiSeparated (f '' s)

theorem Topology.IsOpenEmbedding.isQuasiSeparated_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (h : IsOpenEmbedding 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 t : Set α} (ht : IsQuasiSeparated t) (h : s ⊆ t) : IsQuasiSeparated s

@[instance 100]

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

@[instance 100]

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

theorem QuasiSeparatedSpace.of_isTopologicalBasis {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} {b : ι → Set α} (basis : TopologicalSpace.IsTopologicalBasis (Set.range b)) (isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)) : QuasiSeparatedSpace α

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

theorem QuasiSeparatedSpace.of_isOpenEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [QuasiSeparatedSpace α] {f : β → α} (h : Topology.IsOpenEmbedding f) : QuasiSeparatedSpace β

theorem IsCompact.inter_of_isOpen {α : Type u_1} [TopologicalSpace α] [QuasiSeparatedSpace α] {U V : Set α} (hUcomp : IsCompact U) (hVcomp : IsCompact V) (hUopen : IsOpen U) (hVopen : IsOpen V) : IsCompact (U ∩ V)

theorem quasiSeparatedSpace_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) : QuasiSeparatedSpace α ↔ QuasiSeparatedSpace β