doc-next-gen

Mathlib.Topology.Separation.SeparatedNhds

Module docstring

{"# 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

SeparatedNhds definition
: Set X → Set X → Prop
Full source 
/--
`SeparatedNhds` is a predicate on pairs of sub`Set`s of a topological space.  It holds if the two
sub`Set`s are contained in disjoint open sets.
-/
def SeparatedNhds : Set X → Set X → Prop := fun s t : Set X =>
  ∃ U V : Set X, IsOpen U ∧ IsOpen V ∧ s ⊆ U ∧ t ⊆ V ∧ Disjoint U V
Separation by neighborhoods
Informal description
Two subsets $s$ and $t$ of a topological space $X$ are said to be *separated by neighborhoods* if there exist disjoint open sets $U$ and $V$ in $X$ such that $s \subseteq U$ and $t \subseteq V$.
separatedNhds_iff_disjoint theorem
{s t : Set X} : SeparatedNhds s t ↔ Disjoint (𝓝ˢ s) (𝓝ˢ t)
Full source 
theorem separatedNhds_iff_disjoint {s t : Set X} : SeparatedNhdsSeparatedNhds s t ↔ Disjoint (𝓝ˢ s) (𝓝ˢ t) := by
  simp only [(hasBasis_nhdsSet s).disjoint_iff (hasBasis_nhdsSet t), SeparatedNhds, exists_prop, ←
    exists_and_left, and_assoc, and_comm, and_left_comm]
Equivalence of Neighborhood Separation and Disjoint Neighborhood Filters
Informal description
Two subsets $s$ and $t$ of a topological space $X$ are separated by neighborhoods if and only if their neighborhood filters $\mathcal{N}(s)$ and $\mathcal{N}(t)$ are disjoint, i.e., $\mathcal{N}(s) \cap \mathcal{N}(t) = \emptyset$.
HasSeparatingCover definition
: Set X → Set X → Prop
Full source 
/-- `HasSeparatingCover`s can be useful witnesses for `SeparatedNhds`. -/
def HasSeparatingCover : Set X → Set X → Prop := fun s t ↦
  ∃ u : ℕ → Set X, s ⊆ ⋃ n, u n ∧ ∀ n, IsOpen (u n) ∧ Disjoint (closure (u n)) t
Separating cover of sets in a topological space
Informal description
A set $s$ in a topological space $X$ is said to have a *separating cover* with respect to another set $t$ if there exists a countable family of open sets $(u_n)_{n \in \mathbb{N}}$ such that: 1. $s$ is covered by the union of the $u_n$'s, i.e., $s \subseteq \bigcup_{n} u_n$. 2. For each $n$, the closure of $u_n$ is disjoint from $t$, i.e., $\text{closure}(u_n) \cap t = \emptyset$. This condition is useful for witnessing when two sets can be separated by neighborhoods.
hasSeparatingCovers_iff_separatedNhds theorem
{s t : Set X} : HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t
Full source 
/-- 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 hasSeparatingCovers_iff_separatedNhds {s t : Set X} :
    HasSeparatingCoverHasSeparatingCover s t ∧ HasSeparatingCover t sHasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t := by
  constructor
  · rintro ⟨⟨u, u_cov, u_props⟩, ⟨v, v_cov, v_props⟩⟩
    have open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ n, IsOpen (u₀ n)) →
      IsOpen (⋃ n, u₀ n \ closure (a n)) := fun _ _ u₀i_open ↦
        isOpen_iUnion fun i ↦ (u₀i_open i).sdiff isClosed_closure
    have cover_lemma : ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
        (h₀ ⊆ ⋃ n, u₀ n) → (∀ n, Disjoint (closure (v₀ n)) h₀) →
        (h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m ≤ n, v₀ m)) :=
        fun h₀ u₀ v₀ h₀_cov dis x xinh ↦ by
      rcases h₀_cov xinh with ⟨un , ⟨n, rfl⟩ , xinun⟩
      simp only [mem_iUnion]
      refine ⟨n, xinun, ?_⟩
      simp_all only [closure_iUnion₂_le_nat, disjoint_right, mem_setOf_eq, mem_iUnion,
        exists_false, exists_const, not_false_eq_true]
    refine
      ⟨⋃ n : ℕ, u n \ (closure (⋃ m ≤ n, v m)),
       ⋃ n : ℕ, v n \ (closure (⋃ m ≤ n, u m)),
       open_lemma u (fun n ↦ ⋃ m ≤ n, v m) (fun n ↦ (u_props n).1),
       open_lemma v (fun n ↦ ⋃ m ≤ n, u m) (fun n ↦ (v_props n).1),
       cover_lemma s u v u_cov (fun n ↦ (v_props n).2),
       cover_lemma t v u v_cov (fun n ↦ (u_props n).2),
       ?_⟩
    rw [Set.disjoint_left]
    rintro x ⟨un, ⟨n, rfl⟩, xinun⟩
    suffices ∀ (m : ℕ), x ∈ v m → x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m') by simpa
    intro m xinvm
    have n_le_m : n ≤ m := by
      by_contra m_gt_n
      exact xinun.2 (subset_closure (mem_biUnion (le_of_lt (not_le.mp m_gt_n)) xinvm))
    exact subset_closure (mem_biUnion n_le_m xinun.1)
  · rintro ⟨U, V, U_open, V_open, h_sub_U, k_sub_V, UV_dis⟩
    exact
      ⟨⟨fun _ ↦ U,
        h_sub_U.trans (iUnion_const U).symm.subset,
        fun _ ↦
          ⟨U_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) k_sub_V (UV_dis.closure_left V_open)⟩⟩,
       ⟨fun _ ↦ V,
        k_sub_V.trans (iUnion_const V).symm.subset,
        fun _ ↦
          ⟨V_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) h_sub_U (UV_dis.closure_right U_open).symm⟩⟩⟩
Equivalence of Separating Covers and Neighborhood Separation
Informal description
For any two subsets $s$ and $t$ of a topological space $X$, the following are equivalent: 1. Both $s$ has a separating cover with respect to $t$ and $t$ has a separating cover with respect to $s$. 2. $s$ and $t$ can be separated by neighborhoods (i.e., there exist disjoint open sets $U$ and $V$ such that $s \subseteq U$ and $t \subseteq V$).
HasSeparatingCover.mono theorem
{s₁ s₂ t₁ t₂ : Set X} (sc_st : HasSeparatingCover s₂ t₂) (s_sub : s₁ ⊆ s₂) (t_sub : t₁ ⊆ t₂) : HasSeparatingCover s₁ t₁
Full source 
theorem HasSeparatingCover.mono {s₁ s₂ t₁ t₂ : Set X} (sc_st : HasSeparatingCover s₂ t₂)
    (s_sub : s₁ ⊆ s₂) (t_sub : t₁ ⊆ t₂) : HasSeparatingCover s₁ t₁ := by
  obtain ⟨u, u_cov, u_props⟩ := sc_st
  exact
    ⟨u,
     s_sub.trans u_cov,
     fun n ↦
       ⟨(u_props n).1,
        disjoint_of_subset (fun ⦃_⦄ a ↦ a) t_sub (u_props n).2⟩⟩
Monotonicity of Separating Cover Condition
Informal description
Let $X$ be a topological space and let $s_1, s_2, t_1, t_2$ be subsets of $X$. If $s_2$ and $t_2$ have a separating cover (i.e., there exists a countable family of open sets covering $s_2$ whose closures are disjoint from $t_2$), and if $s_1 \subseteq s_2$ and $t_1 \subseteq t_2$, then $s_1$ and $t_1$ also have a separating cover.
SeparatedNhds.symm theorem
: SeparatedNhds s t → SeparatedNhds t s
Full source 
@[symm]
theorem symm : SeparatedNhds s t → SeparatedNhds t s := fun ⟨U, V, oU, oV, aU, bV, UV⟩ =>
  ⟨V, U, oV, oU, bV, aU, Disjoint.symm UV⟩
Symmetry of Neighborhood Separation
Informal description
If two subsets $s$ and $t$ of a topological space $X$ are separated by neighborhoods, then $t$ and $s$ are also separated by neighborhoods. In other words, the relation of being separated by neighborhoods is symmetric.
SeparatedNhds.comm theorem
(s t : Set X) : SeparatedNhds s t ↔ SeparatedNhds t s
Full source 
theorem comm (s t : Set X) : SeparatedNhdsSeparatedNhds s t ↔ SeparatedNhds t s :=
  ⟨symm, symm⟩
Commutativity of Neighborhood Separation
Informal description
For any two subsets $s$ and $t$ of a topological space $X$, the sets $s$ and $t$ are separated by neighborhoods if and only if $t$ and $s$ are separated by neighborhoods.
SeparatedNhds.preimage theorem
[TopologicalSpace Y] {f : X → Y} {s t : Set Y} (h : SeparatedNhds s t) (hf : Continuous f) : SeparatedNhds (f ⁻¹' s) (f ⁻¹' t)
Full source 
theorem preimage [TopologicalSpace Y] {f : X → Y} {s t : Set Y} (h : SeparatedNhds s t)
    (hf : Continuous f) : SeparatedNhds (f ⁻¹' s) (f ⁻¹' t) :=
  let ⟨U, V, oU, oV, sU, tV, UV⟩ := h
  ⟨f ⁻¹' U, f ⁻¹' V, oU.preimage hf, oV.preimage hf, preimage_mono sU, preimage_mono tV,
    UV.preimage f⟩
Preimage of Separated Neighborhoods under Continuous Map
Informal description
Let $X$ and $Y$ be topological spaces, and let $f : X \to Y$ be a continuous function. If two subsets $s, t \subseteq Y$ are separated by neighborhoods in $Y$, then their preimages $f^{-1}(s)$ and $f^{-1}(t)$ are separated by neighborhoods in $X$.
SeparatedNhds.disjoint theorem
(h : SeparatedNhds s t) : Disjoint s t
Full source 
protected theorem disjoint (h : SeparatedNhds s t) : Disjoint s t :=
  let ⟨_, _, _, _, hsU, htV, hd⟩ := h; hd.mono hsU htV
Disjointness of Sets Separated by Neighborhoods
Informal description
If two subsets $s$ and $t$ of a topological space $X$ are separated by neighborhoods, then they are disjoint, i.e., $s \cap t = \emptyset$.
SeparatedNhds.disjoint_closure_left theorem
(h : SeparatedNhds s t) : Disjoint (closure s) t
Full source 
theorem disjoint_closure_left (h : SeparatedNhds s t) : Disjoint (closure s) t :=
  let ⟨_U, _V, _, hV, hsU, htV, hd⟩ := h
  (hd.closure_left hV).mono (closure_mono hsU) htV
Disjointness of Closure with Separated Neighborhoods
Informal description
If two subsets $s$ and $t$ of a topological space $X$ are separated by neighborhoods, then the closure of $s$ is disjoint from $t$, i.e., $\overline{s} \cap t = \emptyset$.
SeparatedNhds.disjoint_closure_right theorem
(h : SeparatedNhds s t) : Disjoint s (closure t)
Full source 
theorem disjoint_closure_right (h : SeparatedNhds s t) : Disjoint s (closure t) :=
  h.symm.disjoint_closure_left.symm
Disjointness of Set with Closure of Separated Neighborhoods
Informal description
If two subsets $s$ and $t$ of a topological space $X$ are separated by neighborhoods, then $s$ is disjoint from the closure of $t$, i.e., $s \cap \overline{t} = \emptyset$.
SeparatedNhds.empty_left theorem
(s : Set X) : SeparatedNhds ∅ s
Full source 
@[simp] theorem empty_left (s : Set X) : SeparatedNhds ∅ s :=
  (empty_right _).symm
Empty Set is Separated from Any Set by Neighborhoods (Left Version)
Informal description
For any subset $s$ of a topological space $X$, the empty set $\emptyset$ and $s$ are separated by neighborhoods.
SeparatedNhds.mono theorem
(h : SeparatedNhds s₂ t₂) (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : SeparatedNhds s₁ t₁
Full source 
theorem mono (h : SeparatedNhds s₂ t₂) (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : SeparatedNhds s₁ t₁ :=
  let ⟨U, V, hU, hV, hsU, htV, hd⟩ := h
  ⟨U, V, hU, hV, hs.trans hsU, ht.trans htV, hd⟩
Monotonicity of Neighborhood Separation
Informal description
If two subsets $s₂$ and $t₂$ of a topological space $X$ are separated by neighborhoods, and $s₁ \subseteq s₂$, $t₁ \subseteq t₂$, then $s₁$ and $t₁$ are also separated by neighborhoods.
SeparatedNhds.union_left theorem
: SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) u
Full source 
theorem union_left : SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) u := by
  simpa only [separatedNhds_iff_disjoint, nhdsSet_union, disjoint_sup_left] using And.intro
Union of Sets Separated from a Common Set by Neighborhoods
Informal description
For any subsets $s$, $t$, and $u$ of a topological space $X$, if $s$ and $u$ are separated by neighborhoods and $t$ and $u$ are separated by neighborhoods, then the union $s \cup t$ and $u$ are also separated by neighborhoods.
SeparatedNhds.union_right theorem
(ht : SeparatedNhds s t) (hu : SeparatedNhds s u) : SeparatedNhds s (t ∪ u)
Full source 
theorem union_right (ht : SeparatedNhds s t) (hu : SeparatedNhds s u) : SeparatedNhds s (t ∪ u) :=
  (ht.symm.union_left hu.symm).symm
Union of Sets Separated from a Common Set by Neighborhoods (Right Version)
Informal description
For any subsets $s$, $t$, and $u$ of a topological space $X$, if $s$ and $t$ are separated by neighborhoods and $s$ and $u$ are separated by neighborhoods, then $s$ and the union $t \cup u$ are also separated by neighborhoods.
SeparatedNhds.isOpen_left_of_isOpen_union theorem
(hst : SeparatedNhds s t) (hst' : IsOpen (s ∪ t)) : IsOpen s
Full source 
lemma isOpen_left_of_isOpen_union (hst : SeparatedNhds s t) (hst' : IsOpen (s ∪ t)) : IsOpen s := by
  obtain ⟨u, v, hu, hv, hsu, htv, huv⟩ := hst
  suffices s = (s ∪ t) ∩ u from this ▸ hst'.inter hu
  rw [union_inter_distrib_right, (huv.symm.mono_left htv).inter_eq, union_empty,
    inter_eq_left.2 hsu]
Openness of First Set in Separated Neighborhoods with Open Union
Informal description
If two subsets $s$ and $t$ of a topological space $X$ are separated by neighborhoods and their union $s \cup t$ is open, then $s$ is open.
SeparatedNhds.isOpen_right_of_isOpen_union theorem
(hst : SeparatedNhds s t) (hst' : IsOpen (s ∪ t)) : IsOpen t
Full source 
lemma isOpen_right_of_isOpen_union (hst : SeparatedNhds s t) (hst' : IsOpen (s ∪ t)) : IsOpen t :=
  hst.symm.isOpen_left_of_isOpen_union (union_comm _ _ ▸ hst')
Openness of Second Set in Separated Neighborhoods with Open Union
Informal description
If two subsets $s$ and $t$ of a topological space $X$ are separated by neighborhoods and their union $s \cup t$ is open, then $t$ is open.
SeparatedNhds.isOpen_union_iff theorem
(hst : SeparatedNhds s t) : IsOpen (s ∪ t) ↔ IsOpen s ∧ IsOpen t
Full source 
lemma isOpen_union_iff (hst : SeparatedNhds s t) : IsOpenIsOpen (s ∪ t) ↔ IsOpen s ∧ IsOpen t :=
  ⟨fun h ↦ ⟨hst.isOpen_left_of_isOpen_union h, hst.isOpen_right_of_isOpen_union h⟩,
    fun ⟨h1, h2⟩ ↦ h1.union h2⟩
Openness of Union of Separated Sets is Equivalent to Openness of Each Set
Informal description
Let $s$ and $t$ be subsets of a topological space $X$ that are separated by neighborhoods. Then the union $s \cup t$ is open if and only if both $s$ and $t$ are open.
SeparatedNhds.isClosed_left_of_isClosed_union theorem
(hst : SeparatedNhds s t) (hst' : IsClosed (s ∪ t)) : IsClosed s
Full source 
lemma isClosed_left_of_isClosed_union (hst : SeparatedNhds s t) (hst' : IsClosed (s ∪ t)) :
    IsClosed s := by
  obtain ⟨u, v, hu, hv, hsu, htv, huv⟩ := hst
  rw [← isOpen_compl_iff] at hst' ⊢
  suffices sᶜ = (s ∪ t)ᶜ(s ∪ t)ᶜ ∪ v from this ▸ hst'.union hv
  rw [← compl_inj_iff, Set.compl_union, compl_compl, compl_compl, union_inter_distrib_right,
    (disjoint_compl_right.mono_left htv).inter_eq, union_empty, left_eq_inter, subset_compl_comm]
  exact (huv.mono_left hsu).subset_compl_left
Closedness of Separated Set in Closed Union
Informal description
Let $s$ and $t$ be subsets of a topological space $X$ that are separated by neighborhoods. If the union $s \cup t$ is closed, then $s$ is closed.
SeparatedNhds.isClosed_right_of_isClosed_union theorem
(hst : SeparatedNhds s t) (hst' : IsClosed (s ∪ t)) : IsClosed t
Full source 
lemma isClosed_right_of_isClosed_union (hst : SeparatedNhds s t) (hst' : IsClosed (s ∪ t)) :
    IsClosed t :=
  hst.symm.isClosed_left_of_isClosed_union (union_comm _ _ ▸ hst')
Closedness of Right Separated Set in Closed Union
Informal description
Let $s$ and $t$ be subsets of a topological space $X$ that are separated by neighborhoods. If the union $s \cup t$ is closed, then $t$ is closed.
SeparatedNhds.isClosed_union_iff theorem
(hst : SeparatedNhds s t) : IsClosed (s ∪ t) ↔ IsClosed s ∧ IsClosed t
Full source 
lemma isClosed_union_iff (hst : SeparatedNhds s t) : IsClosedIsClosed (s ∪ t) ↔ IsClosed s ∧ IsClosed t :=
  ⟨fun h ↦ ⟨hst.isClosed_left_of_isClosed_union h, hst.isClosed_right_of_isClosed_union h⟩,
    fun ⟨h1, h2⟩ ↦ h1.union h2⟩
Closedness of Union of Separated Sets
Informal description
Let $s$ and $t$ be subsets of a topological space $X$ that are separated by neighborhoods. Then the union $s \cup t$ is closed if and only if both $s$ and $t$ are closed.