doc-next-gen

Mathlib.Topology.DiscreteSubset

Module docstring

{"# Discrete subsets of topological spaces

This file contains various additional properties of discrete subsets of topological spaces.

Discreteness and compact sets

Given a topological space X together with a subset s βŠ† X, there are two distinct concepts of \"discreteness\" which may hold. These are: (i) Every point of s is isolated (i.e., the subset topology induced on s is the discrete topology). (ii) Every compact subset of X meets s only finitely often (i.e., the inclusion map s β†’ X tends to the cocompact filter along the cofinite filter on s).

When s is closed, the two conditions are equivalent provided X is locally compact and T1, see IsClosed.tendsto_coe_cofinite_iff.

Main statements

  • tendsto_cofinite_cocompact_iff:
  • IsClosed.tendsto_coe_cofinite_iff:

Co-discrete open sets

We define the filter Filter.codiscreteWithin S, which is the supremum of all 𝓝[S \\ {x}] x. This is the filter of all open codiscrete sets within S. We also define Filter.codiscrete as Filter.codiscreteWithin univ, which is the filter of all open codiscrete sets in the space.

"}

tendsto_cofinite_cocompact_iff theorem
: Tendsto f cofinite (cocompact _) ↔ βˆ€ K, IsCompact K β†’ Set.Finite (f ⁻¹' K)
Full source 
lemma tendsto_cofinite_cocompact_iff :
    TendstoTendsto f cofinite (cocompact _) ↔ βˆ€ K, IsCompact K β†’ Set.Finite (f ⁻¹' K) := by
  rw [hasBasis_cocompact.tendsto_right_iff]
  refine forallβ‚‚_congr (fun K _ ↦ ?_)
  simp only [mem_compl_iff, eventually_cofinite, not_not, preimage]
Cofinite-to-Cocompact Tendency Criterion
Informal description
A function $f$ tends to the cocompact filter along the cofinite filter if and only if for every compact subset $K$ of the codomain, the preimage $f^{-1}(K)$ is finite.
Continuous.discrete_of_tendsto_cofinite_cocompact theorem
[T1Space X] [WeaklyLocallyCompactSpace Y] (hf' : Continuous f) (hf : Tendsto f cofinite (cocompact _)) : DiscreteTopology X
Full source 
lemma Continuous.discrete_of_tendsto_cofinite_cocompact [T1Space X] [WeaklyLocallyCompactSpace Y]
    (hf' : Continuous f) (hf : Tendsto f cofinite (cocompact _)) :
    DiscreteTopology X := by
  refine singletons_open_iff_discrete.mp (fun x ↦ ?_)
  obtain ⟨K : Set Y, hK : IsCompact K, hK' : K ∈ 𝓝 (f x)⟩ := exists_compact_mem_nhds (f x)
  obtain ⟨U : Set Y, hU₁ : U βŠ† K, hUβ‚‚ : IsOpen U, hU₃ : f x ∈ U⟩ := mem_nhds_iff.mp hK'
  have hUβ‚„ : Set.Finite (f⁻¹' U) :=
    Finite.subset (tendsto_cofinite_cocompact_iff.mp hf K hK) (preimage_mono hU₁)
  exact isOpen_singleton_of_finite_mem_nhds _ ((hUβ‚‚.preimage hf').mem_nhds hU₃) hUβ‚„
Discrete Topology Induced by Cofinite-to-Cocompact Continuous Maps in T₁ Spaces
Informal description
Let $X$ be a T₁ space and $Y$ be a weakly locally compact space. If a continuous function $f \colon X \to Y$ tends to the cocompact filter along the cofinite filter, then $X$ has the discrete topology.
tendsto_cofinite_cocompact_of_discrete theorem
[DiscreteTopology X] (hf : Tendsto f (cocompact _) (cocompact _)) : Tendsto f cofinite (cocompact _)
Full source 
lemma tendsto_cofinite_cocompact_of_discrete [DiscreteTopology X]
    (hf : Tendsto f (cocompact _) (cocompact _)) :
    Tendsto f cofinite (cocompact _) := by
  convert hf
  rw [cocompact_eq_cofinite X]
Cofinite-to-Cocompact Tendency for Discrete Spaces
Informal description
Let $X$ be a topological space with the discrete topology. If a function $f : X \to Y$ tends to the cocompact filter in $Y$ when restricted to the cocompact filter in $X$, then $f$ tends to the cocompact filter in $Y$ along the cofinite filter in $X$.
IsClosed.tendsto_coe_cofinite_of_discreteTopology theorem
{s : Set X} (hs : IsClosed s) (_hs' : DiscreteTopology s) : Tendsto ((↑) : s β†’ X) cofinite (cocompact _)
Full source 
lemma IsClosed.tendsto_coe_cofinite_of_discreteTopology
    {s : Set X} (hs : IsClosed s) (_hs' : DiscreteTopology s) :
    Tendsto ((↑) : s β†’ X) cofinite (cocompact _) :=
  tendsto_cofinite_cocompact_of_discrete hs.isClosedEmbedding_subtypeVal.tendsto_cocompact
Cofinite-to-Cocompact Tendency for Closed Discrete Subsets
Informal description
Let $X$ be a topological space and $s \subseteq X$ be a closed subset with the discrete topology. Then the inclusion map $s \hookrightarrow X$ tends to the cocompact filter on $X$ along the cofinite filter on $s$.
IsClosed.tendsto_coe_cofinite_iff theorem
[T1Space X] [WeaklyLocallyCompactSpace X] {s : Set X} (hs : IsClosed s) : Tendsto ((↑) : s β†’ X) cofinite (cocompact _) ↔ DiscreteTopology s
Full source 
lemma IsClosed.tendsto_coe_cofinite_iff [T1Space X] [WeaklyLocallyCompactSpace X]
    {s : Set X} (hs : IsClosed s) :
    TendstoTendsto ((↑) : s β†’ X) cofinite (cocompact _) ↔ DiscreteTopology s :=
  ⟨continuous_subtype_val.discrete_of_tendsto_cofinite_cocompact,
   fun _ ↦ hs.tendsto_coe_cofinite_of_discreteTopology inferInstance⟩
Equivalence of Cofinite-to-Cocompact Tendency and Discrete Topology for Closed Subsets in T₁ Spaces
Informal description
Let $X$ be a T₁ space that is weakly locally compact, and let $s \subseteq X$ be a closed subset. Then the inclusion map $s \hookrightarrow X$ tends to the cocompact filter along the cofinite filter if and only if $s$ has the discrete topology.
isClosed_and_discrete_iff theorem
{S : Set X} : IsClosed S ∧ DiscreteTopology S ↔ βˆ€ x, Disjoint (𝓝[β‰ ] x) (π“Ÿ S)
Full source 
/-- Criterion for a subset `S βŠ† X` to be closed and discrete in terms of the punctured
neighbourhood filter at an arbitrary point of `X`. (Compare `discreteTopology_subtype_iff`.) -/
theorem isClosed_and_discrete_iff {S : Set X} :
    IsClosedIsClosed S ∧ DiscreteTopology SIsClosed S ∧ DiscreteTopology S ↔ βˆ€ x, Disjoint (𝓝[β‰ ] x) (π“Ÿ S) := by
  rw [discreteTopology_subtype_iff, isClosed_iff_clusterPt, ← forall_and]
  congrm (βˆ€ x, ?_)
  rw [← not_imp_not, clusterPt_iff_not_disjoint, not_not, ← disjoint_iff]
  constructor <;> intro H
  · by_cases hx : x ∈ S
    exacts [H.2 hx, (H.1 hx).mono_left nhdsWithin_le_nhds]
  Β· refine ⟨fun hx ↦ ?_, fun _ ↦ H⟩
    simpa [disjoint_iff, nhdsWithin, inf_assoc, hx] using H
Characterization of Closed Discrete Subsets via Punctured Neighborhoods
Informal description
A subset $S$ of a topological space $X$ is closed and has the discrete topology if and only if for every point $x \in X$, the punctured neighborhood filter at $x$ (denoted $\mathcal{N}[X \setminus \{x\}] x$) is disjoint from the principal filter generated by $S$.
Filter.codiscreteWithin definition
(S : Set X) : Filter X
Full source 
/-- The filter of sets with no accumulation points inside a set `S : Set X`, implemented
as the supremum over all punctured neighborhoods within `S`. -/
def Filter.codiscreteWithin (S : Set X) : Filter X := ⨆ x ∈ S, 𝓝[S \ {x}] x
Filter of codiscrete sets within a subset
Informal description
Given a topological space \( X \) and a subset \( S \subseteq X \), the filter `codiscreteWithin S` is defined as the supremum of the punctured neighborhood filters \( \mathcal{N}[S \setminus \{x\}] x \) for all \( x \in S \). This filter consists of all subsets of \( X \) that have no accumulation points within \( S \).
mem_codiscreteWithin theorem
{S T : Set X} : S ∈ codiscreteWithin T ↔ βˆ€ x ∈ T, Disjoint (𝓝[β‰ ] x) (π“Ÿ (T \ S))
Full source 
lemma mem_codiscreteWithin {S T : Set X} :
    S ∈ codiscreteWithin TS ∈ codiscreteWithin T ↔ βˆ€ x ∈ T, Disjoint (𝓝[β‰ ] x) (π“Ÿ (T \ S)) := by
  simp only [codiscreteWithin, mem_iSup, mem_nhdsWithin, disjoint_principal_right, subset_def,
    mem_diff, mem_inter_iff, mem_compl_iff]
  congr! 7 with x - u y
  tauto
Characterization of Codiscrete Sets via Punctured Neighborhoods
Informal description
A subset $S$ of a topological space $X$ belongs to the filter `codiscreteWithin T` if and only if for every point $x \in T$, the punctured neighborhood filter at $x$ is disjoint from the principal filter generated by $T \setminus S$. In other words, $S$ is in `codiscreteWithin T` precisely when no point in $T$ is an accumulation point of $T \setminus S$.
mem_codiscreteWithin_accPt theorem
{S T : Set X} : S ∈ codiscreteWithin T ↔ βˆ€ x ∈ T, Β¬AccPt x (π“Ÿ (T \ S))
Full source 
lemma mem_codiscreteWithin_accPt {S T : Set X} :
    S ∈ codiscreteWithin TS ∈ codiscreteWithin T ↔ βˆ€ x ∈ T, Β¬AccPt x (π“Ÿ (T \ S)) := by
  simp only [mem_codiscreteWithin, disjoint_iff, AccPt, not_neBot]
Characterization of Codiscrete Sets via Non-Accumulation Points
Informal description
A subset $S$ of a topological space $X$ belongs to the filter $\text{codiscreteWithin}(T)$ if and only if for every point $x \in T$, $x$ is not an accumulation point of the set $T \setminus S$ with respect to the principal filter $\mathcal{P}(T \setminus S)$.
Filter.codiscreteWithin.mono theorem
{U₁ U : Set X} (hU : U₁ βŠ† U) : codiscreteWithin U₁ ≀ codiscreteWithin U
Full source 
/-- If a set is codiscrete within `U`, then it is codiscrete within any subset of `U`. -/
lemma Filter.codiscreteWithin.mono {U₁ U : Set X} (hU : U₁ βŠ† U) :
   codiscreteWithin U₁ ≀ codiscreteWithin U := by
  refine (biSup_mono hU).trans <| iSupβ‚‚_mono fun _ _ ↦ ?_
  gcongr
Monotonicity of Codiscrete Filter with Respect to Subset Inclusion
Informal description
For any subsets $U_1$ and $U$ of a topological space $X$ such that $U_1 \subseteq U$, the filter of codiscrete sets within $U_1$ is finer than the filter of codiscrete sets within $U$, i.e., $\text{codiscreteWithin}(U_1) \leq \text{codiscreteWithin}(U)$.
discreteTopology_of_codiscreteWithin theorem
{U s : Set X} (h : s ∈ Filter.codiscreteWithin U) : DiscreteTopology ((sᢜ ∩ U) : Set X)
Full source 
/-- If `s` is codiscrete within `U`, then `sᢜ ∩ U` has discrete topology. -/
theorem discreteTopology_of_codiscreteWithin {U s : Set X} (h : s ∈ Filter.codiscreteWithin U) :
    DiscreteTopology ((sᢜsᢜ ∩ U) : Set X) := by
  rw [(by simp : ((sᢜ ∩ U) : Set X) = ((s βˆͺ Uᢜ)ᢜ : Set X)), discreteTopology_subtype_iff]
  simp_rw [mem_codiscreteWithin, Filter.disjoint_principal_right] at h
  intro x hx
  rw [← Filter.mem_iff_inf_principal_compl, ← Set.compl_diff]
  simp_all only [h x, Set.compl_union, compl_compl, Set.mem_inter_iff, Set.mem_compl_iff]
Discrete Topology of Complement under Codiscrete Condition
Informal description
Let $X$ be a topological space and $U, s \subseteq X$ be subsets. If $s$ belongs to the codiscrete filter within $U$, then the complement of $s$ intersected with $U$ (i.e., $s^c \cap U$) has the discrete topology.
codiscreteWithin_iff_locallyEmptyComplementWithin theorem
{s U : Set X} : s ∈ codiscreteWithin U ↔ βˆ€ z ∈ U, βˆƒ t ∈ 𝓝[β‰ ] z, t ∩ (U \ s) = βˆ…
Full source 
/-- Helper lemma for `codiscreteWithin_iff_locallyFiniteComplementWithin`: A set `s` is
`codiscreteWithin U` iff every point `z ∈ U` has a punctured neighborhood that does not intersect
`U \ s`. -/
lemma codiscreteWithin_iff_locallyEmptyComplementWithin {s U : Set X} :
    s ∈ codiscreteWithin Us ∈ codiscreteWithin U ↔ βˆ€ z ∈ U, βˆƒ t ∈ 𝓝[β‰ ] z, t ∩ (U \ s) = βˆ… := by
  simp only [mem_codiscreteWithin, disjoint_principal_right]
  refine ⟨fun h z hz ↦ ⟨(U \ s)ᢜ, h z hz, by simp⟩, fun h z hz ↦ ?_⟩
  rw [← exists_mem_subset_iff]
  obtain ⟨t, h₁t, hβ‚‚t⟩ := h z hz
  use t, h₁t, (disjoint_iff_inter_eq_empty.mpr hβ‚‚t).subset_compl_right
Characterization of Codiscrete Sets via Punctured Neighborhoods
Informal description
A subset $s$ of a topological space $X$ belongs to the codiscrete filter within a subset $U \subseteq X$ if and only if for every point $z \in U$, there exists a punctured neighborhood $t$ of $z$ such that $t$ is disjoint from $U \setminus s$.
isClosed_sdiff_of_codiscreteWithin theorem
{s U : Set X} (hs : s ∈ codiscreteWithin U) (hU : IsClosed U) : IsClosed (U \ s)
Full source 
/-- If `U` is closed and `s` is codiscrete within `U`, then `U \ s` is closed. -/
theorem isClosed_sdiff_of_codiscreteWithin {s U : Set X} (hs : s ∈ codiscreteWithin U)
    (hU : IsClosed U) :
    IsClosed (U \ s) := by
  rw [← isOpen_compl_iff, isOpen_iff_eventually]
  intro x hx
  by_cases h₁x : x ∈ U
  Β· rw [mem_codiscreteWithin] at hs
    filter_upwards [eventually_nhdsWithin_iff.1 (disjoint_principal_right.1 (hs x h₁x))]
    intro a ha
    by_cases hβ‚‚a : a = x
    Β· tauto_set
    Β· specialize ha hβ‚‚a
      tauto_set
  Β· rw [eventually_iff_exists_mem]
    use Uᢜ, hU.compl_mem_nhds h₁x
    intro y hy
    tauto_set
Closedness of Set Difference under Codiscrete Condition
Informal description
Let $X$ be a topological space, and let $U, s \subseteq X$ be subsets. If $s$ is codiscrete within $U$ and $U$ is closed, then the set difference $U \setminus s$ is closed.
nhdNE_of_nhdNE_sdiff_finite theorem
{X : Type*} [TopologicalSpace X] [T1Space X] {x : X} {U s : Set X} (hU : U ∈ 𝓝[β‰ ] x) (hs : Finite s) : U \ s ∈ 𝓝[β‰ ] x
Full source 
/-- In a T1Space, punctured neighborhoods are stable under removing finite sets of points. -/
theorem nhdNE_of_nhdNE_sdiff_finite {X : Type*} [TopologicalSpace X] [T1Space X] {x : X}
    {U s : Set X} (hU : U ∈ 𝓝[β‰ ] x) (hs : Finite s) :
    U \ sU \ s ∈ 𝓝[β‰ ] x := by
  rw [mem_nhdsWithin] at hU ⊒
  obtain ⟨t, ht, h₁ts, hβ‚‚ts⟩ := hU
  use t \ (s \ {x})
  constructor
  Β· rw [← isClosed_compl_iff, compl_diff]
    exact hs.diff.isClosed.union (isClosed_compl_iff.2 ht)
  Β· tauto_set
Punctured Neighborhood Stability under Finite Set Removal in T₁ Spaces
Informal description
Let $X$ be a T₁ space, $x \in X$ a point, and $U \subseteq X$ a neighborhood of $x$ punctured at $x$ (i.e., $U \in \mathcal{N}[X \setminus \{x\}] x$). For any finite subset $s \subseteq X$, the set difference $U \setminus s$ remains a punctured neighborhood of $x$.
codiscreteWithin_iff_locallyFiniteComplementWithin theorem
[T1Space X] {s U : Set X} : s ∈ codiscreteWithin U ↔ βˆ€ z ∈ U, βˆƒ t ∈ 𝓝 z, Set.Finite (t ∩ (U \ s))
Full source 
/-- In a T1Space, a set `s` is codiscreteWithin `U` iff it has locally finite complement within `U`.
More precisely: `s` is codiscreteWithin `U` iff every point `z ∈ U` has a punctured neighborhood
intersect `U \ s` in only finitely many points. -/
theorem codiscreteWithin_iff_locallyFiniteComplementWithin [T1Space X] {s U : Set X} :
    s ∈ codiscreteWithin Us ∈ codiscreteWithin U ↔ βˆ€ z ∈ U, βˆƒ t ∈ 𝓝 z, Set.Finite (t ∩ (U \ s)) := by
  rw [codiscreteWithin_iff_locallyEmptyComplementWithin]
  constructor
  Β· intro h z h₁z
    obtain ⟨t, h₁t, hβ‚‚t⟩ := h z h₁z
    use insert z t, insert_mem_nhds_iff.mpr h₁t
    by_cases hz : z ∈ U \ s
    Β· rw [inter_comm, inter_insert_of_mem hz, inter_comm, hβ‚‚t]
      simp
    Β· rw [inter_comm, inter_insert_of_not_mem hz, inter_comm, hβ‚‚t]
      simp
  Β· intro h z h₁z
    obtain ⟨t, h₁t, hβ‚‚t⟩ := h z h₁z
    use t \ (t ∩ (U \ s)), nhdNE_of_nhdNE_sdiff_finite (mem_nhdsWithin_of_mem_nhds h₁t) hβ‚‚t
    simp
Characterization of Codiscrete Sets via Locally Finite Complements in T₁ Spaces
Informal description
Let $X$ be a T₁ space, and let $s, U \subseteq X$ be subsets. Then $s$ is codiscrete within $U$ if and only if for every point $z \in U$, there exists a neighborhood $t$ of $z$ such that the intersection $t \cap (U \setminus s)$ is finite.
Filter.codiscrete definition
(X : Type*) [TopologicalSpace X] : Filter X
Full source 
/-- In any topological space, the open sets with discrete complement form a filter,
defined as the supremum of all punctured neighborhoods.

See `Filter.mem_codiscrete'` for the equivalence. -/
def Filter.codiscrete (X : Type*) [TopologicalSpace X] : Filter X := codiscreteWithin Set.univ
Filter of codiscrete sets
Informal description
The filter `codiscrete` on a topological space \( X \) consists of all subsets \( S \subseteq X \) whose complement has no accumulation points in \( X \). Equivalently, \( S \) belongs to `codiscrete` if for every point \( x \in X \), the punctured neighborhood filter \( \mathcal{N}[X \setminus \{x\}] x \) is disjoint from the principal filter of \( S^c \).
mem_codiscrete theorem
{S : Set X} : S ∈ codiscrete X ↔ βˆ€ x, Disjoint (𝓝[β‰ ] x) (π“Ÿ Sᢜ)
Full source 
lemma mem_codiscrete {S : Set X} :
    S ∈ codiscrete XS ∈ codiscrete X ↔ βˆ€ x, Disjoint (𝓝[β‰ ] x) (π“Ÿ Sᢜ) := by
  simp [codiscrete, mem_codiscreteWithin, compl_eq_univ_diff]
Characterization of Codiscrete Sets via Punctured Neighborhoods
Informal description
A subset $S$ of a topological space $X$ belongs to the filter `codiscrete` if and only if for every point $x \in X$, the punctured neighborhood filter $\mathcal{N}[X \setminus \{x\}] x$ is disjoint from the principal filter generated by the complement $S^c$.
mem_codiscrete_accPt theorem
{S : Set X} : S ∈ codiscrete X ↔ βˆ€ x, Β¬AccPt x (π“Ÿ Sᢜ)
Full source 
lemma mem_codiscrete_accPt {S : Set X} :
    S ∈ codiscrete XS ∈ codiscrete X ↔ βˆ€ x, Β¬AccPt x (π“Ÿ Sᢜ) := by
  simp only [mem_codiscrete, disjoint_iff, AccPt, not_neBot]
Characterization of Codiscrete Sets via Accumulation Points
Informal description
A subset $S$ of a topological space $X$ belongs to the codiscrete filter if and only if no point $x \in X$ is an accumulation point of the complement $S^c$.
mem_codiscrete' theorem
{S : Set X} : S ∈ codiscrete X ↔ IsOpen S ∧ DiscreteTopology ↑Sᢜ
Full source 
lemma mem_codiscrete' {S : Set X} :
    S ∈ codiscrete XS ∈ codiscrete X ↔ IsOpen S ∧ DiscreteTopology ↑Sᢜ := by
  rw [mem_codiscrete, ← isClosed_compl_iff, isClosed_and_discrete_iff]
Characterization of Codiscrete Sets via Openness and Complement's Discrete Topology
Informal description
A subset $S$ of a topological space $X$ belongs to the codiscrete filter if and only if $S$ is open and its complement $S^c$ (viewed as a subspace) has the discrete topology.
mem_codiscrete_subtype_iff_mem_codiscreteWithin theorem
{S : Set X} {U : Set S} : U ∈ codiscrete S ↔ (↑) '' U ∈ codiscreteWithin S
Full source 
lemma mem_codiscrete_subtype_iff_mem_codiscreteWithin {S : Set X} {U : Set S} :
    U ∈ codiscrete SU ∈ codiscrete S ↔ (↑) '' U ∈ codiscreteWithin S := by
  simp [mem_codiscrete, disjoint_principal_right, compl_compl, Subtype.forall,
    mem_codiscreteWithin]
  congr! with x hx
  constructor
  Β· rw [nhdsWithin_subtype, mem_comap]
    rintro ⟨t, ht1, ht2⟩
    rw [mem_nhdsWithin] at ht1 ⊒
    obtain ⟨u, hu1, hu2, hu3⟩ := ht1
    refine ⟨u, hu1, hu2, fun v hv ↦ ?_⟩
    simpa using fun hv2 ↦ ⟨hv2, ht2 <| hu3 <| by simpa [hv2]⟩
  Β· suffices Tendsto (↑) (𝓝[β‰ ] (⟨x, hx⟩ : S)) (𝓝[β‰ ] x) by convert tendsto_def.mp this _; ext; simp
    exact tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      continuous_subtype_val.continuousWithinAt <| eventually_mem_nhdsWithin.mono (by simp)
Equivalence of Codiscrete Filters on Subset and Inclusion Image
Informal description
For any subset $S$ of a topological space $X$ and any subset $U$ of $S$, $U$ belongs to the codiscrete filter on $S$ if and only if the image of $U$ under the inclusion map $S \hookrightarrow X$ belongs to the codiscrete filter within $S$.