Separated neighbourhoods

This file defines the predicates SeparatedNhds and HasSeparatingCover, which are used in formulating separation axioms for topological spaces.

Main definitions

• SeparatedNhds: Two Sets are separated by neighbourhoods if they are contained in disjoint open sets.
• HasSeparatingCover: A set has a countable cover that can be used with hasSeparatingCovers_iff_separatedNhds to witness when two Sets have SeparatedNhds.

References

• https://en.wikipedia.org/wiki/Separation_axiom
• [Willard's General Topology][zbMATH02107988]

def SeparatedNhds {X : Type u_1} [TopologicalSpace X] : Set X → Set X → Prop

SeparatedNhds is a predicate on pairs of subSets of a topological space. It holds if the two subSets are contained in disjoint open sets.

theorem separatedNhds_iff_disjoint {X : Type u_1} [TopologicalSpace X] {s t : Set X} : SeparatedNhds s t ↔ Disjoint (nhdsSet s) (nhdsSet t)

theorem SeparatedNhds.disjoint_nhdsSet {X : Type u_1} [TopologicalSpace X] {s t : Set X} : SeparatedNhds s t → Disjoint (nhdsSet s) (nhdsSet t)

Alias of the forward direction of separatedNhds_iff_disjoint.

def HasSeparatingCover {X : Type u_1} [TopologicalSpace X] : Set X → Set X → Prop

HasSeparatingCovers can be useful witnesses for SeparatedNhds.

theorem hasSeparatingCovers_iff_separatedNhds {X : Type u_1} [TopologicalSpace X] {s t : Set X} : HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t

Used to prove that a regular topological space with Lindelöf topology is a normal space, and a perfectly normal space is a completely normal space.

theorem Set.hasSeparatingCover_empty_left {X : Type u_1} [TopologicalSpace X] (s : Set X) : HasSeparatingCover ∅ s

theorem Set.hasSeparatingCover_empty_right {X : Type u_1} [TopologicalSpace X] (s : Set X) : HasSeparatingCover s ∅

theorem HasSeparatingCover.mono {X : Type u_1} [TopologicalSpace X] {s₁ s₂ t₁ t₂ : Set X} (sc_st : HasSeparatingCover s₂ t₂) (s_sub : s₁ ⊆ s₂) (t_sub : t₁ ⊆ t₂) : HasSeparatingCover s₁ t₁

theorem SeparatedNhds.symm {X : Type u_1} [TopologicalSpace X] {s t : Set X} : SeparatedNhds s t → SeparatedNhds t s

theorem SeparatedNhds.comm {X : Type u_1} [TopologicalSpace X] (s t : Set X) : SeparatedNhds s t ↔ SeparatedNhds t s

theorem SeparatedNhds.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s t : Set Y} (h : SeparatedNhds s t) (hf : Continuous f) : SeparatedNhds (f ⁻¹' s) (f ⁻¹' t)

theorem SeparatedNhds.disjoint {X : Type u_1} [TopologicalSpace X] {s t : Set X} (h : SeparatedNhds s t) : Disjoint s t

theorem SeparatedNhds.disjoint_closure_left {X : Type u_1} [TopologicalSpace X] {s t : Set X} (h : SeparatedNhds s t) : Disjoint (closure s) t

theorem SeparatedNhds.disjoint_closure_right {X : Type u_1} [TopologicalSpace X] {s t : Set X} (h : SeparatedNhds s t) : Disjoint s (closure t)

@[simp]

theorem SeparatedNhds.empty_right {X : Type u_1} [TopologicalSpace X] (s : Set X) : SeparatedNhds s ∅

@[simp]

theorem SeparatedNhds.empty_left {X : Type u_1} [TopologicalSpace X] (s : Set X) : SeparatedNhds ∅ s

theorem SeparatedNhds.mono {X : Type u_1} [TopologicalSpace X] {s₁ s₂ t₁ t₂ : Set X} (h : SeparatedNhds s₂ t₂) (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : SeparatedNhds s₁ t₁

theorem SeparatedNhds.union_left {X : Type u_1} [TopologicalSpace X] {s t u : Set X} : SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) u

theorem SeparatedNhds.union_right {X : Type u_1} [TopologicalSpace X] {s t u : Set X} (ht : SeparatedNhds s t) (hu : SeparatedNhds s u) : SeparatedNhds s (t ∪ u)

theorem SeparatedNhds.isOpen_left_of_isOpen_union {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hst : SeparatedNhds s t) (hst' : IsOpen (s ∪ t)) : IsOpen s

theorem SeparatedNhds.isOpen_right_of_isOpen_union {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hst : SeparatedNhds s t) (hst' : IsOpen (s ∪ t)) : IsOpen t

theorem SeparatedNhds.isOpen_union_iff {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hst : SeparatedNhds s t) : IsOpen (s ∪ t) ↔ IsOpen s ∧ IsOpen t

theorem SeparatedNhds.isClosed_left_of_isClosed_union {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hst : SeparatedNhds s t) (hst' : IsClosed (s ∪ t)) : IsClosed s

theorem SeparatedNhds.isClosed_right_of_isClosed_union {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hst : SeparatedNhds s t) (hst' : IsClosed (s ∪ t)) : IsClosed t

theorem SeparatedNhds.isClosed_union_iff {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hst : SeparatedNhds s t) : IsClosed (s ∪ t) ↔ IsClosed s ∧ IsClosed t