Mathlib.Topology.Separation.Basic

T0Space structure

(X : Type u) [TopologicalSpace X]

Full source

/-- A T₀ space, also known as a Kolmogorov space, is a topological space such that for every pair
`x ≠ y`, there is an open set containing one but not the other. We formulate the definition in terms
of the `Inseparable` relation. -/
class T0Space (X : Type u) [TopologicalSpace X] : Prop where
  /-- Two inseparable points in a T₀ space are equal. -/
  t0 : ∀ ⦃x y : X⦄, Inseparable x y → x = y

T₀ space (Kolmogorov space)

Informal description

A topological space $X$ is called a T₀ space (or Kolmogorov space) if for any two distinct points $x \neq y$ in $X$, there exists an open set that contains one of the points but not the other. This is equivalent to requiring that the relation of topological indistinguishability (i.e., two points are inseparable if they have the same neighborhoods) is trivial, meaning that $x$ and $y$ are inseparable only if $x = y$.

t0Space_iff_inseparable theorem

(X : Type u) [TopologicalSpace X] : T0Space X ↔ ∀ x y : X, Inseparable x y → x = y

Full source

theorem t0Space_iff_inseparable (X : Type u) [TopologicalSpace X] :
    T0SpaceT0Space X ↔ ∀ x y : X, Inseparable x y → x = y :=
  ⟨fun ⟨h⟩ => h, fun h => ⟨h⟩⟩

Characterization of T₀ Spaces via Indistinguishable Points

Informal description

A topological space $X$ is a T₀ space if and only if for any two points $x, y \in X$, if $x$ and $y$ are topologically indistinguishable (i.e., they have the same neighborhoods), then $x = y$.

t0Space_iff_not_inseparable theorem

(X : Type u) [TopologicalSpace X] : T0Space X ↔ Pairwise fun x y : X => ¬Inseparable x y

Full source

theorem t0Space_iff_not_inseparable (X : Type u) [TopologicalSpace X] :
    T0SpaceT0Space X ↔ Pairwise fun x y : X => ¬Inseparable x y := by
  simp only [t0Space_iff_inseparable, Ne, not_imp_not, Pairwise]

Characterization of T₀ Spaces via Non-Inseparability

Informal description

A topological space $X$ is a T₀ space if and only if for every pair of distinct points $x, y \in X$, the points $x$ and $y$ are not topologically indistinguishable (i.e., $\neg \text{Inseparable}(x, y)$).

Inseparable.eq theorem

[T0Space X] {x y : X} (h : Inseparable x y) : x = y

Full source

theorem Inseparable.eq [T0Space X] {x y : X} (h : Inseparable x y) : x = y :=
  T0Space.t0 h

Topological Indistinguishability Implies Equality in T₀ Spaces

Informal description

In a T₀ space $X$, if two points $x$ and $y$ are topologically indistinguishable (i.e., they have the same neighborhoods), then $x = y$.

Topology.IsInducing.injective theorem

[TopologicalSpace Y] [T0Space X] {f : X → Y} (hf : IsInducing f) : Injective f

Full source

/-- A topology inducing map from a T₀ space is injective. -/
protected theorem Topology.IsInducing.injective [TopologicalSpace Y] [T0Space X] {f : X → Y}
    (hf : IsInducing f) : Injective f := fun _ _ h =>
  (hf.inseparable_iff.1 <| .of_eq h).eq

Injectivity of topology-inducing maps from T₀ spaces

Informal description

Let $X$ be a T₀ space and $Y$ a topological space. If $f \colon X \to Y$ is a topology-inducing map (i.e., the topology on $X$ is the coarsest topology making $f$ continuous), then $f$ is injective.

Topology.IsInducing.isEmbedding theorem

[TopologicalSpace Y] [T0Space X] {f : X → Y} (hf : IsInducing f) : IsEmbedding f

Full source

/-- A topology inducing map from a T₀ space is a topological embedding. -/
protected theorem Topology.IsInducing.isEmbedding [TopologicalSpace Y] [T0Space X] {f : X → Y}
    (hf : IsInducing f) : IsEmbedding f :=
  ⟨hf, hf.injective⟩

Topology-inducing maps from T₀ spaces are embeddings

Informal description

Let $X$ be a T₀ space and $Y$ a topological space. If a map $f \colon X \to Y$ is topology-inducing (i.e., the topology on $X$ is the coarsest topology making $f$ continuous), then $f$ is a topological embedding.

isEmbedding_iff_isInducing theorem

[TopologicalSpace Y] [T0Space X] {f : X → Y} : IsEmbedding f ↔ IsInducing f

Full source

lemma isEmbedding_iff_isInducing [TopologicalSpace Y] [T0Space X] {f : X → Y} :
    IsEmbeddingIsEmbedding f ↔ IsInducing f :=
  ⟨IsEmbedding.isInducing, IsInducing.isEmbedding⟩

Characterization of Embeddings via Inducing Topology in T₀ Spaces

Informal description

Let $X$ be a T₀ space and $Y$ a topological space. For a map $f \colon X \to Y$, the following are equivalent: 1. $f$ is a topological embedding (i.e., a homeomorphism onto its image). 2. $f$ is topology-inducing (i.e., the topology on $X$ is the coarsest topology making $f$ continuous).

t0Space_iff_nhds_injective theorem

(X : Type u) [TopologicalSpace X] : T0Space X ↔ Injective (𝓝 : X → Filter X)

Full source

theorem t0Space_iff_nhds_injective (X : Type u) [TopologicalSpace X] :
    T0SpaceT0Space X ↔ Injective (𝓝 : X → Filter X) :=
  t0Space_iff_inseparable X

Characterization of T₀ Spaces via Injectivity of Neighborhood Map

Informal description

A topological space $X$ is a T₀ space if and only if the neighborhood map $\mathcal{N}: X \to \text{Filter } X$ is injective, where $\mathcal{N}(x)$ denotes the neighborhood filter of $x \in X$.

nhds_injective theorem

[T0Space X] : Injective (𝓝 : X → Filter X)

Full source

theorem nhds_injective [T0Space X] : Injective (𝓝 : X → Filter X) :=
  (t0Space_iff_nhds_injective X).1 ‹_›

Injectivity of Neighborhood Map in T₀ Spaces

Informal description

In a T₀ space $X$, the neighborhood map $\mathcal{N}: X \to \text{Filter } X$ is injective, where $\mathcal{N}(x)$ denotes the neighborhood filter of $x \in X$.

inseparable_iff_eq theorem

[T0Space X] {x y : X} : Inseparable x y ↔ x = y

Full source

theorem inseparable_iff_eq [T0Space X] {x y : X} : InseparableInseparable x y ↔ x = y :=
  nhds_injective.eq_iff

Topological Indistinguishability in T₀ Spaces is Equality

Informal description

In a T₀ space $X$, two points $x$ and $y$ are topologically indistinguishable (i.e., have the same neighborhoods) if and only if they are equal, i.e., $\text{Inseparable}(x, y) \leftrightarrow x = y$.

nhds_eq_nhds_iff theorem

[T0Space X] {a b : X} : 𝓝 a = 𝓝 b ↔ a = b

Full source

@[simp]
theorem nhds_eq_nhds_iff [T0Space X] {a b : X} : 𝓝𝓝 a = 𝓝 b ↔ a = b :=
  nhds_injective.eq_iff

Neighborhood Filter Equality Characterizes Equality in T₀ Spaces

Informal description

In a T₀ space $X$, for any two points $a, b \in X$, the neighborhood filters $\mathcal{N}(a)$ and $\mathcal{N}(b)$ are equal if and only if $a = b$.

inseparable_eq_eq theorem

[T0Space X] : Inseparable = @Eq X

Full source

@[simp]
theorem inseparable_eq_eq [T0Space X] : Inseparable = @Eq X :=
  funext₂ fun _ _ => propext inseparable_iff_eq

Topological Indistinguishability Equals Equality in T₀ Spaces

Informal description

In a T₀ space $X$, the relation of topological indistinguishability (denoted by $\text{Inseparable}$) coincides with equality, i.e., $\text{Inseparable}(x, y) \leftrightarrow x = y$ for all $x, y \in X$.

TopologicalSpace.IsTopologicalBasis.inseparable_iff theorem

{b : Set (Set X)} (hb : IsTopologicalBasis b) {x y : X} : Inseparable x y ↔ ∀ s ∈ b, (x ∈ s ↔ y ∈ s)

Full source

theorem TopologicalSpace.IsTopologicalBasis.inseparable_iff {b : Set (Set X)}
    (hb : IsTopologicalBasis b) {x y : X} : InseparableInseparable x y ↔ ∀ s ∈ b, (x ∈ s ↔ y ∈ s) :=
  ⟨fun h _ hs ↦ inseparable_iff_forall_isOpen.1 h _ (hb.isOpen hs),
    fun h ↦ hb.nhds_hasBasis.eq_of_same_basis <| by
      convert hb.nhds_hasBasis using 2
      exact and_congr_right (h _)⟩

Characterization of Topological Indistinguishability via Basis Elements

Informal description

Let $X$ be a topological space with a topological basis $b$. Then two points $x, y \in X$ are topologically indistinguishable (denoted $x \sim y$) if and only if for every basis element $s \in b$, $x \in s$ precisely when $y \in s$.

t0Space_iff_exists_isOpen_xor'_mem theorem

 (X : Type u) [TopologicalSpace X] : T0Space X ↔ Pairwise fun x y => ∃ U : Set X, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U)

Full source

theorem t0Space_iff_exists_isOpen_xor'_mem (X : Type u) [TopologicalSpace X] :
    T0SpaceT0Space X ↔ Pairwise fun x y => ∃ U : Set X, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U) := by
  simp only [t0Space_iff_not_inseparable, xor_iff_not_iff, not_forall, exists_prop,
    inseparable_iff_forall_isOpen, Pairwise]

Characterization of T₀ Spaces via Open Sets

Informal description

A topological space $X$ is a T₀ space if and only if for every pair of distinct points $x, y \in X$, there exists an open set $U \subseteq X$ such that exactly one of $x \in U$ or $y \in U$ holds.

exists_isOpen_xor'_mem theorem

[T0Space X] {x y : X} (h : x ≠ y) : ∃ U : Set X, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U)

Full source

theorem exists_isOpen_xor'_mem [T0Space X] {x y : X} (h : x ≠ y) :
    ∃ U : Set X, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U) :=
  (t0Space_iff_exists_isOpen_xor'_mem X).1 ‹_› h

Existence of Distinguishing Open Set in T₀ Space

Informal description

In a T₀ space $X$, for any two distinct points $x \neq y$, there exists an open set $U \subseteq X$ such that exactly one of $x \in U$ or $y \in U$ holds.

specializationOrder definition

(X) [TopologicalSpace X] [T0Space X] : PartialOrder X

Full source

/-- Specialization forms a partial order on a t0 topological space. -/
def specializationOrder (X) [TopologicalSpace X] [T0Space X] : PartialOrder X :=
  { specializationPreorder X, PartialOrder.lift (OrderDual.toDualOrderDual.toDual ∘ 𝓝) nhds_injective with }

Specialization order on a T₀ space

Informal description

The specialization order on a T₀ topological space $X$ is the partial order defined by $x \leq y$ if every neighborhood of $y$ is a neighborhood of $x$ (equivalently, if $y$ is in the closure of $\{x\}$). In a T₀ space, this order is antisymmetric, making it a genuine partial order.

SeparationQuotient.instT0Space instance

: T0Space (SeparationQuotient X)

Full source

instance SeparationQuotient.instT0Space : T0Space (SeparationQuotient X) :=
  ⟨fun x y => Quotient.inductionOn₂' x y fun _ _ h =>
    SeparationQuotient.mk_eq_mk.2 <| SeparationQuotient.isInducing_mk.inseparable_iff.1 h⟩

Separation Quotient is T₀

Informal description

The separation quotient of a topological space $X$ is a T₀ space.

minimal_nonempty_closed_subsingleton theorem

 [T0Space X] {s : Set X} (hs : IsClosed s) (hmin : ∀ t, t ⊆ s → t.Nonempty → IsClosed t → t = s) : s.Subsingleton

Full source

theorem minimal_nonempty_closed_subsingleton [T0Space X] {s : Set X} (hs : IsClosed s)
    (hmin : ∀ t, t ⊆ s → t.Nonempty → IsClosed t → t = s) : s.Subsingleton := by
  refine fun x hx y hy => of_not_not fun hxy => ?_
  rcases exists_isOpen_xor'_mem hxy with ⟨U, hUo, hU⟩
  wlog h : x ∈ Ux ∈ U ∧ y ∉ U
  · refine this hs hmin y hy x hx (Ne.symm hxy) U hUo hU.symm (hU.resolve_left h)
  obtain ⟨hxU, hyU⟩ := h
  have : s \ U = s := hmin (s \ U) diff_subset ⟨y, hy, hyU⟩ (hs.sdiff hUo)
  exact (this.symm.subset hx).2 hxU

Minimal Nonempty Closed Sets in T₀ Spaces are Singletons

Informal description

Let $X$ be a T₀ space and $s \subseteq X$ a nonempty closed set. If for every nonempty closed subset $t \subseteq s$ we have $t = s$, then $s$ is a singleton set.

minimal_nonempty_closed_eq_singleton theorem

 [T0Space X] {s : Set X} (hs : IsClosed s) (hne : s.Nonempty) (hmin : ∀ t, t ⊆ s → t.Nonempty → IsClosed t → t = s) :
  ∃ x, s = { x }

Full source

theorem minimal_nonempty_closed_eq_singleton [T0Space X] {s : Set X} (hs : IsClosed s)
    (hne : s.Nonempty) (hmin : ∀ t, t ⊆ s → t.Nonempty → IsClosed t → t = s) : ∃ x, s = {x} :=
  exists_eq_singleton_iff_nonempty_subsingleton.2
    ⟨hne, minimal_nonempty_closed_subsingleton hs hmin⟩

Minimal Nonempty Closed Sets in T₀ Spaces are Singletons

Informal description

Let $X$ be a T₀ space and $s \subseteq X$ a nonempty closed set. If for every nonempty closed subset $t \subseteq s$ we have $t = s$, then there exists a point $x \in X$ such that $s = \{x\}$.

IsClosed.exists_closed_singleton theorem

 [T0Space X] [CompactSpace X] {S : Set X} (hS : IsClosed S) (hne : S.Nonempty) :
  ∃ x : X, x ∈ S ∧ IsClosed ({ x } : Set X)

Full source

/-- Given a closed set `S` in a compact T₀ space, there is some `x ∈ S` such that `{x}` is
closed. -/
theorem IsClosed.exists_closed_singleton [T0Space X] [CompactSpace X] {S : Set X}
    (hS : IsClosed S) (hne : S.Nonempty) : ∃ x : X, x ∈ S ∧ IsClosed ({x} : Set X) := by
  obtain ⟨V, Vsub, Vne, Vcls, hV⟩ := hS.exists_minimal_nonempty_closed_subset hne
  rcases minimal_nonempty_closed_eq_singleton Vcls Vne hV with ⟨x, rfl⟩
  exact ⟨x, Vsub (mem_singleton x), Vcls⟩

Existence of Closed Singletons in Nonempty Closed Subsets of Compact T₀ Spaces

Informal description

Let $X$ be a compact T₀ space and $S \subseteq X$ a nonempty closed subset. Then there exists a point $x \in S$ such that the singleton $\{x\}$ is closed in $X$.

minimal_nonempty_open_subsingleton theorem

[T0Space X] {s : Set X} (hs : IsOpen s) (hmin : ∀ t, t ⊆ s → t.Nonempty → IsOpen t → t = s) : s.Subsingleton

Full source

theorem minimal_nonempty_open_subsingleton [T0Space X] {s : Set X} (hs : IsOpen s)
    (hmin : ∀ t, t ⊆ s → t.Nonempty → IsOpen t → t = s) : s.Subsingleton := by
  refine fun x hx y hy => of_not_not fun hxy => ?_
  rcases exists_isOpen_xor'_mem hxy with ⟨U, hUo, hU⟩
  wlog h : x ∈ Ux ∈ U ∧ y ∉ U
  · exact this hs hmin y hy x hx (Ne.symm hxy) U hUo hU.symm (hU.resolve_left h)
  obtain ⟨hxU, hyU⟩ := h
  have : s ∩ U = s := hmin (s ∩ U) inter_subset_left ⟨x, hx, hxU⟩ (hs.inter hUo)
  exact hyU (this.symm.subset hy).2

Minimal Nonempty Open Set in T₀ Space is a Singleton or Empty

Informal description

In a T₀ space $X$, if $s$ is an open set that is minimal with respect to nonempty open subsets (i.e., any nonempty open subset $t \subseteq s$ must equal $s$), then $s$ contains at most one point.

minimal_nonempty_open_eq_singleton theorem

 [T0Space X] {s : Set X} (hs : IsOpen s) (hne : s.Nonempty) (hmin : ∀ t, t ⊆ s → t.Nonempty → IsOpen t → t = s) :
  ∃ x, s = { x }

Full source

theorem minimal_nonempty_open_eq_singleton [T0Space X] {s : Set X} (hs : IsOpen s)
    (hne : s.Nonempty) (hmin : ∀ t, t ⊆ s → t.Nonempty → IsOpen t → t = s) : ∃ x, s = {x} :=
  exists_eq_singleton_iff_nonempty_subsingleton.2 ⟨hne, minimal_nonempty_open_subsingleton hs hmin⟩

Minimal Nonempty Open Set in T₀ Space is a Singleton

Informal description

In a T₀ space $X$, if $s$ is a nonempty open set that is minimal with respect to nonempty open subsets (i.e., any nonempty open subset $t \subseteq s$ must equal $s$), then $s$ is a singleton set. That is, there exists a point $x \in X$ such that $s = \{x\}$.

exists_isOpen_singleton_of_isOpen_finite theorem

[T0Space X] {s : Set X} (hfin : s.Finite) (hne : s.Nonempty) (ho : IsOpen s) : ∃ x ∈ s, IsOpen ({ x } : Set X)

Full source

/-- Given an open finite set `S` in a T₀ space, there is some `x ∈ S` such that `{x}` is open. -/
theorem exists_isOpen_singleton_of_isOpen_finite [T0Space X] {s : Set X} (hfin : s.Finite)
    (hne : s.Nonempty) (ho : IsOpen s) : ∃ x ∈ s, IsOpen ({x} : Set X) := by
  lift s to Finset X using hfin
  induction s using Finset.strongInductionOn
  rename_i s ihs
  rcases em (∃ t, t ⊂ s ∧ t.Nonempty ∧ IsOpen (t : Set X)) with (⟨t, hts, htne, hto⟩ | ht)
  · rcases ihs t hts htne hto with ⟨x, hxt, hxo⟩
    exact ⟨x, hts.1 hxt, hxo⟩
  · -- Porting note: was `rcases minimal_nonempty_open_eq_singleton ho hne _ with ⟨x, hx⟩`
    --               https://github.com/leanprover/std4/issues/116
    rsuffices ⟨x, hx⟩ : ∃ x, s.toSet = {x}
    · exact ⟨x, hx.symm ▸ rfl, hx ▸ ho⟩
    refine minimal_nonempty_open_eq_singleton ho hne ?_
    refine fun t hts htne hto => of_not_not fun hts' => ht ?_
    lift t to Finset X using s.finite_toSet.subset hts
    exact ⟨t, ssubset_iff_subset_ne.2 ⟨hts, mt Finset.coe_inj.2 hts'⟩, htne, hto⟩

Existence of Open Singletons in Finite Open Sets of T₀ Spaces

Informal description

Let $X$ be a T₀ space and $s \subseteq X$ a nonempty finite open set. Then there exists a point $x \in s$ such that the singleton $\{x\}$ is open in $X$.

exists_open_singleton_of_finite theorem

[T0Space X] [Finite X] [Nonempty X] : ∃ x : X, IsOpen ({ x } : Set X)

Full source

theorem exists_open_singleton_of_finite [T0Space X] [Finite X] [Nonempty X] :
    ∃ x : X, IsOpen ({x} : Set X) :=
  let ⟨x, _, h⟩ := exists_isOpen_singleton_of_isOpen_finite (Set.toFinite _)
    univ_nonempty isOpen_univ
  ⟨x, h⟩

Existence of Open Singletons in Finite Nonempty T₀ Spaces

Informal description

Let $X$ be a nonempty finite T₀ space. Then there exists a point $x \in X$ such that the singleton set $\{x\}$ is open in $X$.

t0Space_of_injective_of_continuous theorem

[TopologicalSpace Y] {f : X → Y} (hf : Function.Injective f) (hf' : Continuous f) [T0Space Y] : T0Space X

Full source

theorem t0Space_of_injective_of_continuous [TopologicalSpace Y] {f : X → Y}
    (hf : Function.Injective f) (hf' : Continuous f) [T0Space Y] : T0Space X :=
  ⟨fun _ _ h => hf <| (h.map hf').eq⟩

T₀ Property via Injective Continuous Map

Informal description

Let $X$ and $Y$ be topological spaces, and let $f : X \to Y$ be an injective continuous function. If $Y$ is a T₀ space, then $X$ is also a T₀ space.

Topology.IsEmbedding.t0Space theorem

[TopologicalSpace Y] [T0Space Y] {f : X → Y} (hf : IsEmbedding f) : T0Space X

Full source

protected theorem Topology.IsEmbedding.t0Space [TopologicalSpace Y] [T0Space Y] {f : X → Y}
    (hf : IsEmbedding f) : T0Space X :=
  t0Space_of_injective_of_continuous hf.injective hf.continuous

T₀ Property via Embedding

Informal description

Let $X$ and $Y$ be topological spaces, and let $f : X \to Y$ be an embedding (a continuous injective map that is a homeomorphism onto its image). If $Y$ is a T₀ space, then $X$ is also a T₀ space.

Homeomorph.t0Space theorem

[TopologicalSpace Y] [T0Space X] (h : X ≃ₜ Y) : T0Space Y

Full source

protected theorem Homeomorph.t0Space [TopologicalSpace Y] [T0Space X] (h : X ≃ₜ Y) : T0Space Y :=
  h.symm.isEmbedding.t0Space

Preservation of T₀ Property under Homeomorphism

Informal description

Let $X$ and $Y$ be topological spaces, and let $h: X \to Y$ be a homeomorphism. If $X$ is a T₀ space, then $Y$ is also a T₀ space.

Subtype.t0Space instance

[T0Space X] {p : X → Prop} : T0Space (Subtype p)

Full source

instance Subtype.t0Space [T0Space X] {p : X → Prop} : T0Space (Subtype p) :=
  IsEmbedding.subtypeVal.t0Space

T₀ Property of Subtypes

Informal description

For any T₀ space $X$ and any predicate $p$ on $X$, the subtype $\{x \in X \mid p(x)\}$ is also a T₀ space.

t0Space_iff_or_not_mem_closure theorem

 (X : Type u) [TopologicalSpace X] :
  T0Space X ↔ Pairwise fun a b : X => a ∉ closure ({ b } : Set X) ∨ b ∉ closure ({ a } : Set X)

Full source

theorem t0Space_iff_or_not_mem_closure (X : Type u) [TopologicalSpace X] :
    T0SpaceT0Space X ↔ Pairwise fun a b : X => a ∉ closure ({b} : Set X) ∨ b ∉ closure ({a} : Set X) := by
  simp only [t0Space_iff_not_inseparable, inseparable_iff_mem_closure, not_and_or]

Characterization of T₀ Spaces via Closure Condition

Informal description

A topological space $X$ is a T₀ space if and only if for every pair of distinct points $a, b \in X$, either $a$ is not in the closure of $\{b\}$ or $b$ is not in the closure of $\{a\}$.

Prod.instT0Space instance

[TopologicalSpace Y] [T0Space X] [T0Space Y] : T0Space (X × Y)

Full source

instance Prod.instT0Space [TopologicalSpace Y] [T0Space X] [T0Space Y] : T0Space (X × Y) :=
  ⟨fun _ _ h => Prod.ext (h.map continuous_fst).eq (h.map continuous_snd).eq⟩

Product of T₀ Spaces is T₀

Informal description

For any two topological spaces $X$ and $Y$ that are T₀ spaces, their product space $X \times Y$ is also a T₀ space.

Pi.instT0Space instance

{ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, T0Space (X i)] : T0Space (∀ i, X i)

Full source

instance Pi.instT0Space {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
    [∀ i, T0Space (X i)] :
    T0Space (∀ i, X i) :=
  ⟨fun _ _ h => funext fun i => (h.map (continuous_apply i)).eq⟩

Product of T₀ Spaces is T₀

Informal description

For any family of topological spaces $\{X_i\}_{i \in \iota}$ where each $X_i$ is a T₀ space, the product space $\prod_{i \in \iota} X_i$ is also a T₀ space.

ULift.instT0Space instance

[T0Space X] : T0Space (ULift X)

Full source

instance ULift.instT0Space [T0Space X] : T0Space (ULift X) := IsEmbedding.uliftDown.t0Space

Lifted T₀ Space is T₀

Informal description

For any T₀ space $X$, the lifted space $\mathrm{ULift}\, X$ (which represents $X$ in a different universe) is also a T₀ space.

T0Space.of_cover theorem

(h : ∀ x y, Inseparable x y → ∃ s : Set X, x ∈ s ∧ y ∈ s ∧ T0Space s) : T0Space X

Full source

theorem T0Space.of_cover (h : ∀ x y, Inseparable x y → ∃ s : Set X, x ∈ s ∧ y ∈ s ∧ T0Space s) :
    T0Space X := by
  refine ⟨fun x y hxy => ?_⟩
  rcases h x y hxy with ⟨s, hxs, hys, hs⟩
  lift x to s using hxs; lift y to s using hys
  rw [← subtype_inseparable_iff] at hxy
  exact congr_arg Subtype.val hxy.eq

T₀ Space Characterization via Local T₀ Subsets

Informal description

A topological space $X$ is a T₀ space if for any two points $x, y \in X$ that are topologically indistinguishable (i.e., $x$ and $y$ have the same neighborhoods), there exists a subset $s \subseteq X$ containing both $x$ and $y$ such that $s$ with the subspace topology is a T₀ space.

T0Space.of_open_cover theorem

(h : ∀ x, ∃ s : Set X, x ∈ s ∧ IsOpen s ∧ T0Space s) : T0Space X

Full source

theorem T0Space.of_open_cover (h : ∀ x, ∃ s : Set X, x ∈ s ∧ IsOpen s ∧ T0Space s) : T0Space X :=
  T0Space.of_cover fun x _ hxy =>
    let ⟨s, hxs, hso, hs⟩ := h x
    ⟨s, hxs, (hxy.mem_open_iff hso).1 hxs, hs⟩

T₀ Space Characterization via Open T₀ Covers

Informal description

A topological space $X$ is a T₀ space if for every point $x \in X$, there exists an open subset $s \subseteq X$ containing $x$ such that $s$ with the subspace topology is a T₀ space.

R0Space structure

(X : Type u) [TopologicalSpace X]

Full source

/-- A topological space is called an R₀ space, if `Specializes` relation is symmetric.

In other words, given two points `x y : X`,
if every neighborhood of `y` contains `x`, then every neighborhood of `x` contains `y`. -/
@[mk_iff]
class R0Space (X : Type u) [TopologicalSpace X] : Prop where
  /-- In an R₀ space, the `Specializes` relation is symmetric. -/
  specializes_symmetric : Symmetric (Specializes : X → X → Prop)

R₀ Space (Symmetric Space)

Informal description

A topological space $X$ is called an R₀ space (or symmetric space) if the specialization relation is symmetric. That is, for any two points $x, y \in X$, if every neighborhood of $y$ contains $x$ (written $x \preceq y$), then every neighborhood of $x$ contains $y$ (written $y \preceq x$).

Specializes.symm theorem

(h : x ⤳ y) : y ⤳ x

Full source

/-- In an R₀ space, the `Specializes` relation is symmetric, dot notation version. -/
theorem Specializes.symm (h : x ⤳ y) : y ⤳ x := specializes_symmetric h

Symmetry of Specialization Relation in R₀ Spaces

Informal description

In an R₀ space, the specialization relation is symmetric: if $x$ specializes to $y$ (denoted $x \preceq y$), then $y$ specializes to $x$ (denoted $y \preceq x$).

specializes_comm theorem

: x ⤳ y ↔ y ⤳ x

Full source

/-- In an R₀ space, the `Specializes` relation is symmetric, `Iff` version. -/
theorem specializes_comm : x ⤳ yx ⤳ y ↔ y ⤳ x := ⟨Specializes.symm, Specializes.symm⟩

Symmetry of Specialization Relation in R₀ Spaces

Informal description

In an R₀ space, the specialization relation is symmetric: for any two points $x$ and $y$, $x$ specializes to $y$ if and only if $y$ specializes to $x$, i.e., $x \preceq y \leftrightarrow y \preceq x$.

specializes_iff_inseparable theorem

: x ⤳ y ↔ Inseparable x y

Full source

/-- In an R₀ space, `Specializes` is equivalent to `Inseparable`. -/
theorem specializes_iff_inseparable : x ⤳ yx ⤳ y ↔ Inseparable x y :=
  ⟨fun h ↦ h.antisymm h.symm, Inseparable.specializes⟩

Specialization Equivalence to Inseparability in R₀ Spaces

Informal description

In an R₀ space, for any two points $x$ and $y$, the specialization relation $x \preceq y$ holds if and only if $x$ and $y$ are topologically inseparable (i.e., they have the same closure).

Topology.IsInducing.r0Space theorem

[TopologicalSpace Y] {f : Y → X} (hf : IsInducing f) : R0Space Y

Full source

theorem Topology.IsInducing.r0Space [TopologicalSpace Y] {f : Y → X} (hf : IsInducing f) :
    R0Space Y where
  specializes_symmetric a b := by
    simpa only [← hf.specializes_iff] using Specializes.symm

Induced Topology Preserves R₀ Property

Informal description

Let $Y$ be a topological space and $f : Y \to X$ be an inducing map (i.e., the topology on $Y$ is the coinduced topology from $f$). If $X$ is an R₀ space, then $Y$ is also an R₀ space.

instR0SpaceSubtype instance

{p : X → Prop} : R0Space { x // p x }

Full source

instance {p : X → Prop} : R0Space {x // p x} := IsInducing.subtypeVal.r0Space

Subtype of an R₀ Space is R₀

Informal description

For any topological space $X$ and any predicate $p$ on $X$, the subtype $\{x \in X \mid p(x)\}$ is an R₀ space when equipped with the subspace topology.

instR0SpaceProd instance

[TopologicalSpace Y] [R0Space Y] : R0Space (X × Y)

Full source

instance [TopologicalSpace Y] [R0Space Y] : R0Space (X × Y) where
  specializes_symmetric _ _ h := h.fst.symm.prod h.snd.symm

Product of R₀ Spaces is R₀

Informal description

For any topological spaces $X$ and $Y$ where $Y$ is an R₀ space, the product space $X \times Y$ is also an R₀ space.

instR0SpaceForall instance

{ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, R0Space (X i)] : R0Space (∀ i, X i)

Full source

instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, R0Space (X i)] :
    R0Space (∀ i, X i) where
  specializes_symmetric _ _ h := specializes_pi.2 fun i ↦ (specializes_pi.1 h i).symm

Product of R₀ Spaces is R₀

Informal description

For any family of topological spaces $\{X_i\}_{i \in \iota}$ where each $X_i$ is an R₀ space, the product space $\prod_{i \in \iota} X_i$ is also an R₀ space.

isCompact_closure_singleton theorem

: IsCompact (closure { x })

Full source

/-- In an R₀ space, the closure of a singleton is a compact set. -/
theorem isCompact_closure_singleton : IsCompact (closure {x}) := by
  refine isCompact_of_finite_subcover fun U hUo hxU ↦ ?_
  obtain ⟨i, hi⟩ : ∃ i, x ∈ U i := mem_iUnion.1 <| hxU <| subset_closure rfl
  refine ⟨{i}, fun y hy ↦ ?_⟩
  rw [← specializes_iff_mem_closure, specializes_comm] at hy
  simpa using hy.mem_open (hUo i) hi

Compactness of Singleton Closures in R₀ Spaces

Informal description

In an R₀ space, the closure of any singleton set $\{x\}$ is compact.

Filter.coclosedCompact_le_cofinite theorem

: coclosedCompact X ≤ cofinite

Full source

theorem Filter.coclosedCompact_le_cofinite : coclosedCompact X ≤ cofinite :=
  le_cofinite_iff_compl_singleton_mem.2 fun _ ↦
    compl_mem_coclosedCompact.2 isCompact_closure_singleton

Coclosed-Compact Filter is Finer than Cofinite Filter

Informal description

In any topological space $X$, the coclosed-compact filter is finer than the cofinite filter. That is, every set in the coclosed-compact filter has a finite complement.

Bornology.relativelyCompact definition

: Bornology X

Full source

/-- In an R₀ space, relatively compact sets form a bornology.
Its cobounded filter is `Filter.coclosedCompact`.
See also `Bornology.inCompact` the bornology of sets contained in a compact set. -/
def Bornology.relativelyCompact : Bornology X where
  cobounded' := Filter.coclosedCompact X
  le_cofinite' := Filter.coclosedCompact_le_cofinite

Relatively compact bornology

Informal description

The bornology on a topological space $X$ where the bounded sets are precisely those whose closure is compact. The cobounded filter for this bornology is the coclosed-compact filter, which consists of sets whose complement is closed and compact. This bornology is finer than the cofinite bornology, meaning every set with compact closure has finite complement.

Bornology.relativelyCompact.isBounded_iff theorem

{s : Set X} : @Bornology.IsBounded _ (Bornology.relativelyCompact X) s ↔ IsCompact (closure s)

Full source

theorem Bornology.relativelyCompact.isBounded_iff {s : Set X} :
    @Bornology.IsBounded _ (Bornology.relativelyCompact X) s ↔ IsCompact (closure s) :=
  compl_mem_coclosedCompact

Characterization of Bounded Sets in Relatively Compact Bornology via Closure

Informal description

For any subset $s$ of a topological space $X$, $s$ is bounded in the relatively compact bornology if and only if the closure of $s$ is compact. That is, $\text{IsBounded}(s) \leftrightarrow \text{IsCompact}(\overline{s})$.

Set.Finite.isCompact_closure theorem

{s : Set X} (hs : s.Finite) : IsCompact (closure s)

Full source

/-- In an R₀ space, the closure of a finite set is a compact set. -/
theorem Set.Finite.isCompact_closure {s : Set X} (hs : s.Finite) : IsCompact (closure s) :=
  let _ : Bornology X := .relativelyCompact X
  Bornology.relativelyCompact.isBounded_iff.1 hs.isBounded

Compactness of Closure of Finite Sets in R₀ Spaces

Informal description

In an R₀ space $X$, the closure of any finite subset $s \subseteq X$ is compact.

T1Space structure

(X : Type u) [TopologicalSpace X]

Full source

/-- A T₁ space, also known as a Fréchet space, is a topological space
  where every singleton set is closed. Equivalently, for every pair
  `x ≠ y`, there is an open set containing `x` and not `y`. -/
class T1Space (X : Type u) [TopologicalSpace X] : Prop where
  /-- A singleton in a T₁ space is a closed set. -/
  t1 : ∀ x, IsClosed ({x} : Set X)

T₁ space (Fréchet space)

Informal description

A topological space $ X $ is called a T₁ space (or Fréchet space) if every singleton set $\{x\}$ is closed in $ X $. Equivalently, for any two distinct points $ x \neq y $ in $ X $, there exists an open set containing $ x $ but not $ y $.

isClosed_singleton theorem

[T1Space X] {x : X} : IsClosed ({ x } : Set X)

Full source

theorem isClosed_singleton [T1Space X] {x : X} : IsClosed ({x} : Set X) :=
  T1Space.t1 x

Closedness of Singletons in T₁ Spaces

Informal description

In a T₁ space $ X $, every singleton set $\{x\}$ is closed.

isOpen_compl_singleton theorem

[T1Space X] {x : X} : IsOpen ({ x }ᶜ : Set X)

Full source

theorem isOpen_compl_singleton [T1Space X] {x : X} : IsOpen ({x}{x}ᶜ : Set X) :=
  isClosed_singleton.isOpen_compl

Openness of Singleton Complements in T₁ Spaces

Informal description

In a T₁ space $ X $, the complement of any singleton set $\{x\}$ is open.

isOpen_ne theorem

[T1Space X] {x : X} : IsOpen {y | y ≠ x}

Full source

theorem isOpen_ne [T1Space X] {x : X} : IsOpen { y | y ≠ x } :=
  isOpen_compl_singleton

Openness of the Complement of a Point in a T₁ Space

Informal description

In a T₁ space $X$, for any point $x \in X$, the set $\{y \in X \mid y \neq x\}$ is open.

Continuous.isOpen_mulSupport theorem

[T1Space X] [One X] [TopologicalSpace Y] {f : Y → X} (hf : Continuous f) : IsOpen (mulSupport f)

Full source

@[to_additive]
theorem Continuous.isOpen_mulSupport [T1Space X] [One X] [TopologicalSpace Y] {f : Y → X}
    (hf : Continuous f) : IsOpen (mulSupport f) :=
  isOpen_ne.preimage hf

Openness of Multiplicative Support for Continuous Functions in T₁ Spaces

Informal description

Let $X$ be a T₁ space with a distinguished element $1 \in X$, and let $Y$ be a topological space. For any continuous function $f : Y \to X$, the multiplicative support $\operatorname{mulSupport}(f) = \{y \in Y \mid f(y) \neq 1\}$ is an open subset of $Y$.

Ne.nhdsWithin_compl_singleton theorem

[T1Space X] {x y : X} (h : x ≠ y) : 𝓝[{ y }ᶜ] x = 𝓝 x

Full source

theorem Ne.nhdsWithin_compl_singleton [T1Space X] {x y : X} (h : x ≠ y) : 𝓝[{y}ᶜ] x = 𝓝 x :=
  isOpen_ne.nhdsWithin_eq h

Neighborhood Filter Equality at a Point Outside a Singleton in a T₁ Space

Informal description

In a T₁ space $X$, for any two distinct points $x \neq y$, the neighborhood filter of $x$ restricted to the complement of $\{y\}$ is equal to the unrestricted neighborhood filter of $x$.

Ne.nhdsWithin_diff_singleton theorem

[T1Space X] {x y : X} (h : x ≠ y) (s : Set X) : 𝓝[s \ { y }] x = 𝓝[s] x

Full source

theorem Ne.nhdsWithin_diff_singleton [T1Space X] {x y : X} (h : x ≠ y) (s : Set X) :
    𝓝[s \ {y}] x = 𝓝[s] x := by
  rw [diff_eq, inter_comm, nhdsWithin_inter_of_mem]
  exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)

Neighborhood Filter Equality in T₁ Space upon Point Removal

Informal description

Let $X$ be a T₁ space, and let $x, y \in X$ be distinct points ($x \neq y$). For any subset $s \subseteq X$, the neighborhood filter of $x$ within $s \setminus \{y\}$ is equal to the neighborhood filter of $x$ within $s$.

nhdsWithin_compl_singleton_le theorem

[T1Space X] (x y : X) : 𝓝[{ x }ᶜ] x ≤ 𝓝[{ y }ᶜ] x

Full source

lemma nhdsWithin_compl_singleton_le [T1Space X] (x y : X) : 𝓝[{x}ᶜ] x ≤ 𝓝[{y}ᶜ] x := by
  rcases eq_or_ne x y with rfl|hy
  · exact Eq.le rfl
  · rw [Ne.nhdsWithin_compl_singleton hy]
    exact nhdsWithin_le_nhds

Comparison of Neighborhood Filters in T₁ Space upon Point Removal

Informal description

In a T₁ space $X$, for any two points $x, y \in X$, the neighborhood filter of $x$ restricted to the complement of $\{x\}$ is finer than the neighborhood filter of $x$ restricted to the complement of $\{y\}$. In other words, $\mathcal{N}_{\{x\}^c}(x) \leq \mathcal{N}_{\{y\}^c}(x)$.

isOpen_setOf_eventually_nhdsWithin theorem

[T1Space X] {p : X → Prop} : IsOpen {x | ∀ᶠ y in 𝓝[≠] x, p y}

Full source

theorem isOpen_setOf_eventually_nhdsWithin [T1Space X] {p : X → Prop} :
    IsOpen { x | ∀ᶠ y in 𝓝[≠] x, p y } := by
  refine isOpen_iff_mem_nhds.mpr fun a ha => ?_
  filter_upwards [eventually_nhds_nhdsWithin.mpr ha] with b hb
  rcases eq_or_ne a b with rfl | h
  · exact hb
  · rw [h.symm.nhdsWithin_compl_singleton] at hb
    exact hb.filter_mono nhdsWithin_le_nhds

Openness of Points Where Predicate Eventually Holds in Punctured Neighborhoods in T₁ Spaces

Informal description

In a T₁ space $X$, for any predicate $p : X \to \text{Prop}$, the set $\{x \in X \mid \text{eventually } p \text{ holds in the punctured neighborhood of } x\}$ is open.

Set.Finite.isClosed theorem

[T1Space X] {s : Set X} (hs : s.Finite) : IsClosed s

Full source

@[simp] protected lemma Set.Finite.isClosed [T1Space X] {s : Set X} (hs : s.Finite) :
    IsClosed s := by
  rw [← biUnion_of_singleton s]
  exact hs.isClosed_biUnion fun i _ => isClosed_singleton

Closedness of Finite Subsets in T₁ Spaces

Informal description

In a T₁ space $ X $, every finite subset $ s \subseteq X $ is closed.

Finset.isClosed theorem

[T1Space X] (s : Finset X) : IsClosed (s : Set X)

Full source

protected theorem Finset.isClosed [T1Space X] (s : Finset X) : IsClosed (s : Set X) :=
  s.finite_toSet.isClosed

Closedness of Finsets in T₁ Spaces

Informal description

In a T₁ space $ X $, every finite subset $ s \subseteq X $ represented as a finset is closed in the topological space.

t1Space_TFAE theorem

 (X : Type u) [TopologicalSpace X] :
  List.TFAE
    [T1Space X, ∀ x, IsClosed ({ x } : Set X), ∀ x, IsOpen ({ x }ᶜ : Set X), Continuous (@CofiniteTopology.of X),
      ∀ ⦃x y : X⦄, x ≠ y → { y }ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y]

Full source

theorem t1Space_TFAE (X : Type u) [TopologicalSpace X] :
    List.TFAE [T1Space X,
      ∀ x, IsClosed ({ x } : Set X),
      ∀ x, IsOpen ({ x }ᶜ : Set X),
      Continuous (@CofiniteTopology.of X),
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y] := by
  tfae_have 1 ↔ 2 := ⟨fun h => h.1, fun h => ⟨h⟩⟩
  tfae_have 2 ↔ 3 := by
    simp only [isOpen_compl_iff]
  tfae_have 5 ↔ 3 := by
    refine forall_swap.trans ?_
    simp only [isOpen_iff_mem_nhds, mem_compl_iff, mem_singleton_iff]
  tfae_have 5 ↔ 6 := by
    simp only [← subset_compl_singleton_iff, exists_mem_subset_iff]
  tfae_have 5 ↔ 7 := by
    simp only [(nhds_basis_opens _).mem_iff, subset_compl_singleton_iff, exists_prop, and_assoc,
      and_left_comm]
  tfae_have 5 ↔ 8 := by
    simp only [← principal_singleton, disjoint_principal_right]
  tfae_have 8 ↔ 9 := forall_swap.trans (by simp only [disjoint_comm, ne_comm])
  tfae_have 1 → 4 := by
    simp only [continuous_def, CofiniteTopology.isOpen_iff']
    rintro H s (rfl | hs)
    exacts [isOpen_empty, compl_compl s ▸ (@Set.Finite.isClosed _ _ H _ hs).isOpen_compl]
  tfae_have 4 → 2 :=
    fun h x => (CofiniteTopology.isClosed_iff.2 <| Or.inr (finite_singleton _)).preimage h
  tfae_have 2 ↔ 10 := by
    simp only [← closure_subset_iff_isClosed, specializes_iff_mem_closure, subset_def,
      mem_singleton_iff, eq_comm]
  tfae_finish

Equivalent Characterizations of T₁ Spaces

Informal description

For a topological space $ X $, the following statements are equivalent: 1. $ X $ is a T₁ space. 2. Every singleton set $\{x\}$ is closed in $ X $. 3. The complement of every singleton set $\{x\}$ is open in $ X $. 4. The canonical map from $ X $ to the cofinite topology is continuous. 5. For any two distinct points $ x \neq y $, the complement of $\{y\}$ is a neighborhood of $ x $. 6. For any two distinct points $ x \neq y $, there exists a neighborhood of $ x $ not containing $ y $. 7. For any two distinct points $ x \neq y $, there exists an open set $ U $ containing $ x $ but not $ y $. 8. For any two distinct points $ x \neq y $, the neighborhood filter of $ x $ and the principal filter of $ y $ are disjoint. 9. For any two distinct points $ x \neq y $, the principal filter of $ x $ and the neighborhood filter of $ y $ are disjoint. 10. For any two points $ x $ and $ y $, if $ x $ specializes to $ y $, then $ x = y $.

t1Space_iff_continuous_cofinite_of theorem

: T1Space X ↔ Continuous (@CofiniteTopology.of X)

Full source

theorem t1Space_iff_continuous_cofinite_of : T1SpaceT1Space X ↔ Continuous (@CofiniteTopology.of X) :=
  (t1Space_TFAE X).out 0 3

T₁ Space Characterization via Cofinite Topology Continuity

Informal description

A topological space $X$ is a T₁ space if and only if the canonical map from $X$ to the cofinite topology is continuous.

CofiniteTopology.continuous_of theorem

[T1Space X] : Continuous (@CofiniteTopology.of X)

Full source

theorem CofiniteTopology.continuous_of [T1Space X] : Continuous (@CofiniteTopology.of X) :=
  t1Space_iff_continuous_cofinite_of.mp ‹_›

Continuity of the Cofinite Topology Map in T₁ Spaces

Informal description

If a topological space $X$ is a T₁ space, then the canonical map from $X$ to the cofinite topology is continuous.

t1Space_iff_exists_open theorem

: T1Space X ↔ Pairwise fun x y => ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ y ∉ U

Full source

theorem t1Space_iff_exists_open :
    T1SpaceT1Space X ↔ Pairwise fun x y => ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ y ∉ U :=
  (t1Space_TFAE X).out 0 6

Characterization of T₁ Spaces via Open Sets

Informal description

A topological space $X$ is a T₁ space if and only if for every pair of distinct points $x \neq y$ in $X$, there exists an open set $U$ such that $x \in U$ and $y \notin U$.

t1Space_iff_disjoint_pure_nhds theorem

: T1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)

Full source

theorem t1Space_iff_disjoint_pure_nhds : T1SpaceT1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y) :=
  (t1Space_TFAE X).out 0 8

T₁ space characterization via disjoint filters

Informal description

A topological space $X$ is a T₁ space if and only if for any two distinct points $x \neq y$ in $X$, the principal filter $\{x\}$ and the neighborhood filter of $y$ are disjoint.

t1Space_iff_disjoint_nhds_pure theorem

: T1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)

Full source

theorem t1Space_iff_disjoint_nhds_pure : T1SpaceT1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y) :=
  (t1Space_TFAE X).out 0 7

T₁ Space Characterization via Disjoint Neighborhood and Principal Filters

Informal description

A topological space $X$ is a T₁ space if and only if for any two distinct points $x \neq y$ in $X$, the neighborhood filter of $x$ and the principal filter of $y$ are disjoint.

t1Space_iff_specializes_imp_eq theorem

: T1Space X ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y

Full source

theorem t1Space_iff_specializes_imp_eq : T1SpaceT1Space X ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y :=
  (t1Space_TFAE X).out 0 9

T₁ Space Characterization via Specialization Relation

Informal description

A topological space $X$ is a T₁ space if and only if for any two points $x, y \in X$, the specialization relation $x \rightsquigarrow y$ implies $x = y$.

disjoint_pure_nhds theorem

[T1Space X] {x y : X} (h : x ≠ y) : Disjoint (pure x) (𝓝 y)

Full source

theorem disjoint_pure_nhds [T1Space X] {x y : X} (h : x ≠ y) : Disjoint (pure x) (𝓝 y) :=
  t1Space_iff_disjoint_pure_nhds.mp ‹_› h

Disjointness of Principal and Neighborhood Filters in T₁ Spaces

Informal description

In a T₁ space $X$, for any two distinct points $x \neq y$, the principal filter $\{x\}$ and the neighborhood filter of $y$ are disjoint.

disjoint_nhds_pure theorem

[T1Space X] {x y : X} (h : x ≠ y) : Disjoint (𝓝 x) (pure y)

Full source

theorem disjoint_nhds_pure [T1Space X] {x y : X} (h : x ≠ y) : Disjoint (𝓝 x) (pure y) :=
  t1Space_iff_disjoint_nhds_pure.mp ‹_› h

Disjointness of Neighborhood and Principal Filters in T₁ Spaces

Informal description

In a T₁ space $X$, for any two distinct points $x \neq y$, the neighborhood filter of $x$ and the principal filter of $y$ are disjoint.

Specializes.eq theorem

[T1Space X] {x y : X} (h : x ⤳ y) : x = y

Full source

theorem Specializes.eq [T1Space X] {x y : X} (h : x ⤳ y) : x = y :=
  t1Space_iff_specializes_imp_eq.1 ‹_› h

Specialization Implies Equality in T₁ Spaces

Informal description

In a T₁ space $ X $, if a point $ x $ specializes to a point $ y $ (denoted $ x \rightsquigarrow y $), then $ x = y $.

specializes_iff_eq theorem

[T1Space X] {x y : X} : x ⤳ y ↔ x = y

Full source

theorem specializes_iff_eq [T1Space X] {x y : X} : x ⤳ yx ⤳ y ↔ x = y :=
  ⟨Specializes.eq, fun h => h ▸ specializes_rfl⟩

Specialization Equals Equality in T₁ Spaces

Informal description

In a T₁ space $X$, for any two points $x$ and $y$, the specialization relation $x \rightsquigarrow y$ holds if and only if $x = y$.

specializes_eq_eq theorem

[T1Space X] : (· ⤳ ·) = @Eq X

Full source

@[simp] theorem specializes_eq_eq [T1Space X] : (· ⤳ ·) = @Eq X :=
  funext₂ fun _ _ => propext specializes_iff_eq

Specialization Relation Equals Equality in T₁ Spaces

Informal description

In a T₁ space $X$, the specialization relation $\rightsquigarrow$ coincides with equality, i.e., for any $x, y \in X$, $x \rightsquigarrow y$ if and only if $x = y$.

pure_le_nhds_iff theorem

[T1Space X] {a b : X} : pure a ≤ 𝓝 b ↔ a = b

Full source

@[simp]
theorem pure_le_nhds_iff [T1Space X] {a b : X} : purepure a ≤ 𝓝 b ↔ a = b :=
  specializes_iff_pure.symm.trans specializes_iff_eq

Principal Filter Containment in Neighborhood Filter Characterizes Equality in T₁ Spaces

Informal description

In a T₁ space $X$, for any two points $a$ and $b$, the principal filter $\{a\}$ is contained in the neighborhood filter of $b$ if and only if $a = b$.

nhds_le_nhds_iff theorem

[T1Space X] {a b : X} : 𝓝 a ≤ 𝓝 b ↔ a = b

Full source

@[simp]
theorem nhds_le_nhds_iff [T1Space X] {a b : X} : 𝓝𝓝 a ≤ 𝓝 b ↔ a = b :=
  specializes_iff_eq

Neighborhood Filter Containment Criterion in T₁ Spaces

Informal description

In a T₁ space $X$, for any two points $a$ and $b$, the neighborhood filter of $a$ is contained in the neighborhood filter of $b$ if and only if $a = b$.

instR0SpaceOfT1Space instance

[T1Space X] : R0Space X

Full source

instance (priority := 100) [T1Space X] : R0Space X where
  specializes_symmetric _ _ := by rw [specializes_iff_eq, specializes_iff_eq]; exact Eq.symm

T₁ Spaces are R₀ Spaces

Informal description

Every T₁ space is an R₀ space.

instT1SpaceCofiniteTopology instance

: T1Space (CofiniteTopology X)

Full source

instance : T1Space (CofiniteTopology X) :=
  t1Space_iff_continuous_cofinite_of.mpr continuous_id

Cofinite Topology is T₁

Informal description

The cofinite topology on any type $X$ is a T₁ space. That is, for any two distinct points $x \neq y$ in $X$ equipped with the cofinite topology, there exists an open set containing $x$ but not $y$.

t1Space_antitone theorem

{X} : Antitone (@T1Space X)

Full source

theorem t1Space_antitone {X} : Antitone (@T1Space X) := fun a _ h _ =>
  @T1Space.mk _ a fun x => (T1Space.t1 x).mono h

Antitone Property of T₁ Spaces with Respect to Coarser Topologies

Informal description

For any topological space $X$, the property of being a T₁ space is antitone with respect to the coarser-than relation on topologies. That is, if $\tau_1$ and $\tau_2$ are topologies on $X$ with $\tau_1 \subseteq \tau_2$, and $(X, \tau_2)$ is a T₁ space, then $(X, \tau_1)$ is also a T₁ space.

continuousWithinAt_update_of_ne theorem

 [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {x x' : X} {y : Y} (hne : x' ≠ x) :
  ContinuousWithinAt (Function.update f x y) s x' ↔ ContinuousWithinAt f s x'

Full source

theorem continuousWithinAt_update_of_ne [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : X → Y}
    {s : Set X} {x x' : X} {y : Y} (hne : x' ≠ x) :
    ContinuousWithinAtContinuousWithinAt (Function.update f x y) s x' ↔ ContinuousWithinAt f s x' :=
  EventuallyEq.congr_continuousWithinAt
    (mem_nhdsWithin_of_mem_nhds <| mem_of_superset (isOpen_ne.mem_nhds hne) fun _y' hy' =>
      Function.update_of_ne hy' _ _)
    (Function.update_of_ne hne ..)

Continuity Within a Set of a Function Update at a Distinct Point in a T₁ Space

Informal description

Let $X$ be a T₁ space with a decidable equality, and let $Y$ be a topological space. For any function $f : X \to Y$, any subset $s \subseteq X$, any distinct points $x, x' \in X$ with $x' \neq x$, and any $y \in Y$, the following equivalence holds: \[ \text{The function } \text{update } f \, x \, y \text{ is continuous within } s \text{ at } x' \text{ if and only if } f \text{ is continuous within } s \text{ at } x'. \] Here, $\text{update } f \, x \, y$ denotes the function that coincides with $f$ everywhere except at $x$, where it takes the value $y$.

continuousAt_update_of_ne theorem

 [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : X → Y} {x x' : X} {y : Y} (hne : x' ≠ x) :
  ContinuousAt (Function.update f x y) x' ↔ ContinuousAt f x'

Full source

theorem continuousAt_update_of_ne [T1Space X] [DecidableEq X] [TopologicalSpace Y]
    {f : X → Y} {x x' : X} {y : Y} (hne : x' ≠ x) :
    ContinuousAtContinuousAt (Function.update f x y) x' ↔ ContinuousAt f x' := by
  simp only [← continuousWithinAt_univ, continuousWithinAt_update_of_ne hne]

Continuity of Function Update at Distinct Points in T₁ Spaces

Informal description

Let $X$ be a T₁ space with decidable equality, and let $Y$ be a topological space. For any function $f : X \to Y$, any distinct points $x, x' \in X$ with $x' \neq x$, and any $y \in Y$, the following equivalence holds: \[ \text{The function } f \text{ updated at } x \text{ with value } y \text{ is continuous at } x' \text{ if and only if } f \text{ is continuous at } x'. \] Here, the updated function is defined as $f'(a) = y$ if $a = x$ and $f'(a) = f(a)$ otherwise.

continuousOn_update_iff theorem

 [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {x : X} {y : Y} :
  ContinuousOn (Function.update f x y) s ↔ ContinuousOn f (s \ { x }) ∧ (x ∈ s → Tendsto f (𝓝[s \ { x }] x) (𝓝 y))

Full source

theorem continuousOn_update_iff [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : X → Y}
    {s : Set X} {x : X} {y : Y} :
    ContinuousOnContinuousOn (Function.update f x y) s ↔
      ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y)) := by
  rw [ContinuousOn, ← and_forall_ne x, and_comm]
  refine and_congr ⟨fun H z hz => ?_, fun H z hzx hzs => ?_⟩ (forall_congr' fun _ => ?_)
  · specialize H z hz.2 hz.1
    rw [continuousWithinAt_update_of_ne hz.2] at H
    exact H.mono diff_subset
  · rw [continuousWithinAt_update_of_ne hzx]
    refine (H z ⟨hzs, hzx⟩).mono_of_mem_nhdsWithin (inter_mem_nhdsWithin _ ?_)
    exact isOpen_ne.mem_nhds hzx
  · exact continuousWithinAt_update_same

Continuity of Function Update on a Set in T₁ Space

Informal description

Let $X$ be a T₁ space with decidable equality, $Y$ a topological space, $f : X \to Y$ a function, $s \subseteq X$ a subset, $x \in X$ a point, and $y \in Y$ a value. Then the following equivalence holds: \[ \text{The updated function } f_{x \mapsto y} \text{ is continuous on } s \text{ if and only if } f \text{ is continuous on } s \setminus \{x\} \text{ and, when } x \in s, \text{ the limit of } f \text{ at } x \text{ within } s \setminus \{x\} \text{ is } y. \] Here $f_{x \mapsto y}$ denotes the function equal to $f$ everywhere except at $x$ where it takes value $y$.

t1Space_of_injective_of_continuous theorem

[TopologicalSpace Y] {f : X → Y} (hf : Function.Injective f) (hf' : Continuous f) [T1Space Y] : T1Space X

Full source

theorem t1Space_of_injective_of_continuous [TopologicalSpace Y] {f : X → Y}
    (hf : Function.Injective f) (hf' : Continuous f) [T1Space Y] : T1Space X :=
  t1Space_iff_specializes_imp_eq.2 fun _ _ h => hf (h.map hf').eq

T₁ Space Induced by Injective Continuous Map from T₁ Space

Informal description

Let $X$ and $Y$ be topological spaces, and let $f : X \to Y$ be an injective continuous function. If $Y$ is a T₁ space, then $X$ is also a T₁ space.

Topology.IsEmbedding.t1Space theorem

[TopologicalSpace Y] [T1Space Y] {f : X → Y} (hf : IsEmbedding f) : T1Space X

Full source

protected theorem Topology.IsEmbedding.t1Space [TopologicalSpace Y] [T1Space Y] {f : X → Y}
    (hf : IsEmbedding f) : T1Space X :=
  t1Space_of_injective_of_continuous hf.injective hf.continuous

T₁ Space Property Preserved Under Embedding from T₁ Space

Informal description

Let $X$ and $Y$ be topological spaces, with $Y$ being a T₁ space. If $f: X \to Y$ is an embedding (a continuous injective map that is a homeomorphism onto its image), then $X$ is also a T₁ space.

Homeomorph.t1Space theorem

[TopologicalSpace Y] [T1Space X] (h : X ≃ₜ Y) : T1Space Y

Full source

protected theorem Homeomorph.t1Space [TopologicalSpace Y] [T1Space X] (h : X ≃ₜ Y) : T1Space Y :=
  h.symm.isEmbedding.t1Space

T₁ Space Property Preserved Under Homeomorphism

Informal description

Let $X$ and $Y$ be topological spaces, with $X$ being a T₁ space. If $h: X \to Y$ is a homeomorphism, then $Y$ is also a T₁ space.

Subtype.t1Space instance

{X : Type u} [TopologicalSpace X] [T1Space X] {p : X → Prop} : T1Space (Subtype p)

Full source

instance Subtype.t1Space {X : Type u} [TopologicalSpace X] [T1Space X] {p : X → Prop} :
    T1Space (Subtype p) :=
  IsEmbedding.subtypeVal.t1Space

Subspace of a T₁ Space is T₁

Informal description

For any topological space $X$ that is a T₁ space and any predicate $p$ on $X$, the subspace $\{x \in X \mid p(x)\}$ is also a T₁ space.

instT1SpaceProd instance

[TopologicalSpace Y] [T1Space X] [T1Space Y] : T1Space (X × Y)

Full source

instance [TopologicalSpace Y] [T1Space X] [T1Space Y] : T1Space (X × Y) :=
  ⟨fun ⟨a, b⟩ => @singleton_prod_singleton _ _ a b ▸ isClosed_singleton.prod isClosed_singleton⟩

Product of T₁ Spaces is T₁

Informal description

For any two topological spaces $X$ and $Y$ that are T₁ spaces, their product $X \times Y$ is also a T₁ space.

instT1SpaceForall instance

{ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, T1Space (X i)] : T1Space (∀ i, X i)

Full source

instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, T1Space (X i)] :
    T1Space (∀ i, X i) :=
  ⟨fun f => univ_pi_singleton f ▸ isClosed_set_pi fun _ _ => isClosed_singleton⟩

Product of T₁ Spaces is T₁

Informal description

For any family of topological spaces $\{X_i\}_{i \in \iota}$ where each $X_i$ is a T₁ space, the product space $\prod_{i \in \iota} X_i$ is also a T₁ space.

ULift.instT1Space instance

[T1Space X] : T1Space (ULift X)

Full source

instance ULift.instT1Space [T1Space X] : T1Space (ULift X) :=
  IsEmbedding.uliftDown.t1Space

T₁ Space Property Preserved Under Lifting

Informal description

For any T₁ space $X$, the lifted space $\text{ULift}\, X$ is also a T₁ space.

T1Space.t0Space instance

[T1Space X] : T0Space X

Full source

instance (priority := 100) T1Space.t0Space [T1Space X] : T0Space X :=
  ⟨fun _ _ h => h.specializes.eq⟩

T₁ Spaces are T₀ Spaces

Informal description

Every T₁ space is also a T₀ space.

compl_singleton_mem_nhds_iff theorem

[T1Space X] {x y : X} : { x }ᶜ ∈ 𝓝 y ↔ y ≠ x

Full source

@[simp]
theorem compl_singleton_mem_nhds_iff [T1Space X] {x y : X} : {x}{x}ᶜ{x}ᶜ ∈ 𝓝 y{x}ᶜ ∈ 𝓝 y ↔ y ≠ x :=
  isOpen_compl_singleton.mem_nhds_iff

Neighborhood Condition for Singleton Complements in T₁ Spaces

Informal description

In a T₁ space $ X $, for any two points $ x $ and $ y $, the complement of the singleton set $\{x\}$ is a neighborhood of $ y $ if and only if $ y \neq x $. In other words, $\{x\}^c \in \mathcal{N}(y) \leftrightarrow y \neq x$, where $\mathcal{N}(y)$ denotes the neighborhood filter at $ y $.

compl_singleton_mem_nhds theorem

[T1Space X] {x y : X} (h : y ≠ x) : { x }ᶜ ∈ 𝓝 y

Full source

theorem compl_singleton_mem_nhds [T1Space X] {x y : X} (h : y ≠ x) : {x}{x}ᶜ{x}ᶜ ∈ 𝓝 y :=
  compl_singleton_mem_nhds_iff.mpr h

Neighborhood Property of Singleton Complements in T₁ Spaces

Informal description

In a T₁ space $X$, for any two distinct points $x$ and $y$ (i.e., $y \neq x$), the complement of the singleton set $\{x\}$ is a neighborhood of $y$.

closure_singleton theorem

[T1Space X] {x : X} : closure ({ x } : Set X) = { x }

Full source

theorem closure_singleton [T1Space X] {x : X} : closure ({x} : Set X) = {x} :=
  isClosed_singleton.closure_eq

Closure of Singletons in T₁ Spaces

Informal description

In a T₁ space $X$, the closure of any singleton set $\{x\}$ is equal to itself, i.e., $\overline{\{x\}} = \{x\}$.

Set.Subsingleton.isClosed theorem

[T1Space X] {s : Set X} (hs : s.Subsingleton) : IsClosed s

Full source

lemma Set.Subsingleton.isClosed [T1Space X] {s : Set X} (hs : s.Subsingleton) : IsClosed s := by
  rcases hs.eq_empty_or_singleton with rfl | ⟨x, rfl⟩
  · exact isClosed_empty
  · exact isClosed_singleton

Closedness of Subsingleton Sets in T₁ Spaces

Informal description

In a T₁ space $ X $, every subsingleton set $ s $ (i.e., a set containing at most one point) is closed.

Set.Subsingleton.closure_eq theorem

[T1Space X] {s : Set X} (hs : s.Subsingleton) : closure s = s

Full source

theorem Set.Subsingleton.closure_eq [T1Space X] {s : Set X} (hs : s.Subsingleton) :
    closure s = s :=
  hs.isClosed.closure_eq

Closure of Subsingleton Sets in T₁ Spaces Equals the Set Itself

Informal description

In a T₁ space $X$, for any subsingleton set $s \subseteq X$ (i.e., a set containing at most one point), the closure of $s$ is equal to $s$ itself, i.e., $\overline{s} = s$.

Set.Subsingleton.closure theorem

[T1Space X] {s : Set X} (hs : s.Subsingleton) : (closure s).Subsingleton

Full source

theorem Set.Subsingleton.closure [T1Space X] {s : Set X} (hs : s.Subsingleton) :
    (closure s).Subsingleton := by
  rwa [hs.closure_eq]

Closure Preserves Subsingleton Property in T₁ Spaces

Informal description

In a T₁ space $X$, the closure of any subsingleton set $s$ (i.e., a set containing at most one point) is also a subsingleton set.

subsingleton_closure theorem

[T1Space X] {s : Set X} : (closure s).Subsingleton ↔ s.Subsingleton

Full source

@[simp]
theorem subsingleton_closure [T1Space X] {s : Set X} : (closure s).Subsingleton ↔ s.Subsingleton :=
  ⟨fun h => h.anti subset_closure, fun h => h.closure⟩

Subsingleton Property of Closure in T₁ Spaces

Informal description

In a T₁ space $X$, the closure $\overline{s}$ of a subset $s \subseteq X$ is a subsingleton (i.e., contains at most one point) if and only if $s$ itself is a subsingleton.

isClosedMap_const theorem

{X Y} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {y : Y} : IsClosedMap (Function.const X y)

Full source

theorem isClosedMap_const {X Y} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {y : Y} :
    IsClosedMap (Function.const X y) :=
  IsClosedMap.of_nonempty fun s _ h2s => by simp_rw [const, h2s.image_const, isClosed_singleton]

Constant Maps are Closed in T₁ Spaces

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ being a T₁ space. Then for any fixed point $y \in Y$, the constant function $f_y: X \to Y$ defined by $f_y(x) = y$ for all $x \in X$ is a closed map (i.e., it maps closed sets in $X$ to closed sets in $Y$).

isClosedMap_prodMk_left theorem

[TopologicalSpace Y] [T1Space X] (x : X) : IsClosedMap (fun y : Y ↦ Prod.mk x y)

Full source

lemma isClosedMap_prodMk_left [TopologicalSpace Y] [T1Space X] (x : X) :
    IsClosedMap (fun y : Y ↦ Prod.mk x y) :=
  fun _K hK ↦ Set.singleton_prod ▸ isClosed_singleton.prod hK

Left Projection Map is Closed in T₁ Spaces

Informal description

Let $X$ and $Y$ be topological spaces with $X$ being a T₁ space. Then for any fixed point $x \in X$, the function $f_x: Y \to X \times Y$ defined by $f_x(y) = (x, y)$ is a closed map (i.e., it maps closed sets in $Y$ to closed sets in $X \times Y$).

isClosedMap_prodMk_right theorem

[TopologicalSpace Y] [T1Space Y] (y : Y) : IsClosedMap (fun x : X ↦ Prod.mk x y)

Full source

lemma isClosedMap_prodMk_right [TopologicalSpace Y] [T1Space Y] (y : Y) :
    IsClosedMap (fun x : X ↦ Prod.mk x y) :=
  fun _K hK ↦ Set.prod_singleton ▸ hK.prod isClosed_singleton

Right Projection Map is Closed in T₁ Spaces

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ being a T₁ space. Then for any fixed point $y \in Y$, the function $f_y: X \to X \times Y$ defined by $f_y(x) = (x, y)$ is a closed map (i.e., it maps closed sets in $X$ to closed sets in $X \times Y$).

nhdsWithin_insert_of_ne theorem

[T1Space X] {x y : X} {s : Set X} (hxy : x ≠ y) : 𝓝[insert y s] x = 𝓝[s] x

Full source

theorem nhdsWithin_insert_of_ne [T1Space X] {x y : X} {s : Set X} (hxy : x ≠ y) :
    𝓝[insert y s] x = 𝓝[s] x := by
  refine le_antisymm (Filter.le_def.2 fun t ht => ?_) (nhdsWithin_mono x <| subset_insert y s)
  obtain ⟨o, ho, hxo, host⟩ := mem_nhdsWithin.mp ht
  refine mem_nhdsWithin.mpr ⟨o \ {y}, ho.sdiff isClosed_singleton, ⟨hxo, hxy⟩, ?_⟩
  rw [inter_insert_of_not_mem <| not_mem_diff_of_mem (mem_singleton y)]
  exact (inter_subset_inter diff_subset Subset.rfl).trans host

Neighborhood Filter within Inserted Point in T₁ Spaces

Informal description

Let $X$ be a T₁ space, and let $x, y \in X$ be distinct points ($x \neq y$). For any subset $s \subseteq X$, the neighborhood filter of $x$ within the set $\{y\} \cup s$ is equal to the neighborhood filter of $x$ within $s$.

insert_mem_nhdsWithin_of_subset_insert theorem

[T1Space X] {x y : X} {s t : Set X} (hu : t ⊆ insert y s) : insert x s ∈ 𝓝[t] x

Full source

/-- If `t` is a subset of `s`, except for one point,
then `insert x s` is a neighborhood of `x` within `t`. -/
theorem insert_mem_nhdsWithin_of_subset_insert [T1Space X] {x y : X} {s t : Set X}
    (hu : t ⊆ insert y s) : insertinsert x s ∈ 𝓝[t] x := by
  rcases eq_or_ne x y with (rfl | h)
  · exact mem_of_superset self_mem_nhdsWithin hu
  refine nhdsWithin_mono x hu ?_
  rw [nhdsWithin_insert_of_ne h]
  exact mem_of_superset self_mem_nhdsWithin (subset_insert x s)

Neighborhood Property of Insertion in T₁ Spaces

Informal description

Let $X$ be a T₁ space, and let $x, y \in X$ be points (not necessarily distinct). For any subsets $s, t \subseteq X$ such that $t \subseteq \{y\} \cup s$, the set $\{x\} \cup s$ is a neighborhood of $x$ within $t$.

eventuallyEq_insert theorem

 [T1Space X] {s t : Set X} {x y : X} (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) : (insert x s : Set X) =ᶠ[𝓝 x] (insert x t : Set X)

Full source

lemma eventuallyEq_insert [T1Space X] {s t : Set X} {x y : X} (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
    (insert x s : Set X) =ᶠ[𝓝 x] (insert x t : Set X) := by
  simp_rw [eventuallyEq_set] at h ⊢
  simp_rw [← union_singleton, ← nhdsWithin_univ, ← compl_union_self {x},
    nhdsWithin_union, eventually_sup, nhdsWithin_singleton,
    eventually_pure, union_singleton, mem_insert_iff, true_or, and_true]
  filter_upwards [nhdsWithin_compl_singleton_le x y h] with y using or_congr (Iff.rfl)

Eventual Equality of Inserted Sets in T₁ Spaces

Informal description

Let $X$ be a T₁ space, and let $s, t \subseteq X$ be subsets. For any points $x, y \in X$, if $s$ and $t$ are eventually equal in the neighborhood filter of $x$ restricted to the complement of $\{y\}$, then the sets $\{x\} \cup s$ and $\{x\} \cup t$ are eventually equal in the full neighborhood filter of $x$. In other words, if $s = t$ for all points sufficiently close to $x$ (excluding $y$ if $x = y$), then $\{x\} \cup s = \{x\} \cup t$ for all points sufficiently close to $x$.

ker_nhds theorem

[T1Space X] (x : X) : (𝓝 x).ker = { x }

Full source

@[simp]
theorem ker_nhds [T1Space X] (x : X) : (𝓝 x).ker = {x} := by
  simp [ker_nhds_eq_specializes]

Kernel of Neighborhood Filter in T₁ Space is Singleton

Informal description

In a T₁ space $X$, for any point $x \in X$, the kernel of the neighborhood filter of $x$ is equal to the singleton set $\{x\}$. Here, the kernel of a filter $\mathcal{F}$ is defined as the intersection of all sets in $\mathcal{F}$.

biInter_basis_nhds theorem

 [T1Space X] {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {x : X} (h : (𝓝 x).HasBasis p s) : ⋂ (i) (_ : p i), s i = { x }

Full source

theorem biInter_basis_nhds [T1Space X] {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {x : X}
    (h : (𝓝 x).HasBasis p s) : ⋂ (i) (_ : p i), s i = {x} := by
  rw [← h.ker, ker_nhds]

Intersection of Basis Sets in T₁ Space is Singleton

Informal description

Let $X$ be a T₁ space, and let $\{s_i\}_{i \in \iota}$ be a family of subsets of $X$ indexed by a type $\iota$, with a predicate $p : \iota \to \text{Prop}$. For a point $x \in X$, if the neighborhood filter $\mathcal{N}(x)$ has a basis $\{s_i \mid p(i)\}$, then the intersection of all $s_i$ for which $p(i)$ holds is exactly the singleton set $\{x\}$. In other words, $\bigcap_{i, p(i)} s_i = \{x\}$.

compl_singleton_mem_nhdsSet_iff theorem

[T1Space X] {x : X} {s : Set X} : { x }ᶜ ∈ 𝓝ˢ s ↔ x ∉ s

Full source

@[simp]
theorem compl_singleton_mem_nhdsSet_iff [T1Space X] {x : X} {s : Set X} : {x}{x}ᶜ{x}ᶜ ∈ 𝓝ˢ s{x}ᶜ ∈ 𝓝ˢ s ↔ x ∉ s := by
  rw [isOpen_compl_singleton.mem_nhdsSet, subset_compl_singleton_iff]

Neighborhood Criterion for Singleton Complements in T₁ Spaces

Informal description

In a T₁ space $X$, for any point $x \in X$ and any subset $s \subseteq X$, the complement of the singleton $\{x\}$ is a neighborhood of $s$ if and only if $x$ does not belong to $s$. In other words, $\{x\}^c \in \mathcal{N}(s) \leftrightarrow x \notin s$.

nhdsSet_le_iff theorem

[T1Space X] {s t : Set X} : 𝓝ˢ s ≤ 𝓝ˢ t ↔ s ⊆ t

Full source

@[simp]
theorem nhdsSet_le_iff [T1Space X] {s t : Set X} : 𝓝ˢ𝓝ˢ s ≤ 𝓝ˢ t ↔ s ⊆ t := by
  refine ⟨?_, fun h => monotone_nhdsSet h⟩
  simp_rw [Filter.le_def]; intro h x hx
  specialize h {x}{x}ᶜ
  simp_rw [compl_singleton_mem_nhdsSet_iff] at h
  by_contra hxt
  exact h hxt hx

Neighborhood Filter Ordering in T₁ Spaces

Informal description

In a T₁ space $ X $, for any subsets $ s $ and $ t $ of $ X $, the neighborhood filter of $ s $ is less than or equal to the neighborhood filter of $ t $ if and only if $ s $ is a subset of $ t $. In other words, $ \mathcal{N}(s) \leq \mathcal{N}(t) \leftrightarrow s \subseteq t $.

nhdsSet_inj_iff theorem

[T1Space X] {s t : Set X} : 𝓝ˢ s = 𝓝ˢ t ↔ s = t

Full source

@[simp]
theorem nhdsSet_inj_iff [T1Space X] {s t : Set X} : 𝓝ˢ𝓝ˢ s = 𝓝ˢ t ↔ s = t := by
  simp_rw [le_antisymm_iff]
  exact and_congr nhdsSet_le_iff nhdsSet_le_iff

Neighborhood Filter Equality in T₁ Spaces Characterizes Set Equality

Informal description

In a T₁ space $ X $, for any subsets $ s $ and $ t $ of $ X $, the neighborhood filter of $ s $ is equal to the neighborhood filter of $ t $ if and only if $ s = t $. In other words, $ \mathcal{N}(s) = \mathcal{N}(t) \leftrightarrow s = t $.

injective_nhdsSet theorem

[T1Space X] : Function.Injective (𝓝ˢ : Set X → Filter X)

Full source

theorem injective_nhdsSet [T1Space X] : Function.Injective (𝓝ˢ : Set X → Filter X) := fun _ _ hst =>
  nhdsSet_inj_iff.mp hst

Injectivity of Neighborhood Filter Function in T₁ Spaces

Informal description

In a T₁ space $X$, the neighborhood filter function $\mathcal{N}^s : \mathcal{P}(X) \to \text{Filter}(X)$ is injective. That is, for any subsets $s, t \subseteq X$, if $\mathcal{N}^s(s) = \mathcal{N}^s(t)$, then $s = t$.

strictMono_nhdsSet theorem

[T1Space X] : StrictMono (𝓝ˢ : Set X → Filter X)

Full source

theorem strictMono_nhdsSet [T1Space X] : StrictMono (𝓝ˢ : Set X → Filter X) :=
  monotone_nhdsSet.strictMono_of_injective injective_nhdsSet

Strict Monotonicity of Neighborhood Filters in T₁ Spaces

Informal description

In a T₁ space $X$, the neighborhood filter function $\mathcal{N}^s : \mathcal{P}(X) \to \text{Filter}(X)$ is strictly monotone. That is, for any subsets $s, t \subseteq X$, if $s \subsetneq t$, then $\mathcal{N}^s(s) \subsetneq \mathcal{N}^s(t)$.

nhds_le_nhdsSet_iff theorem

[T1Space X] {s : Set X} {x : X} : 𝓝 x ≤ 𝓝ˢ s ↔ x ∈ s

Full source

@[simp]
theorem nhds_le_nhdsSet_iff [T1Space X] {s : Set X} {x : X} : 𝓝𝓝 x ≤ 𝓝ˢ s ↔ x ∈ s := by
  rw [← nhdsSet_singleton, nhdsSet_le_iff, singleton_subset_iff]

Neighborhood Filter Comparison in T₁ Spaces: $ \mathcal{N}(x) \leq \mathcal{N}(s) \leftrightarrow x \in s $

Informal description

In a T₁ space $ X $, for any subset $ s \subseteq X $ and any point $ x \in X $, the neighborhood filter of $ x $ is less than or equal to the neighborhood filter of $ s $ if and only if $ x $ belongs to $ s $. In other words, $ \mathcal{N}(x) \leq \mathcal{N}(s) \leftrightarrow x \in s $.

Dense.diff_singleton theorem

[T1Space X] {s : Set X} (hs : Dense s) (x : X) [NeBot (𝓝[≠] x)] : Dense (s \ { x })

Full source

/-- Removing a non-isolated point from a dense set, one still obtains a dense set. -/
theorem Dense.diff_singleton [T1Space X] {s : Set X} (hs : Dense s) (x : X) [NeBot (𝓝[≠] x)] :
    Dense (s \ {x}) :=
  hs.inter_of_isOpen_right (dense_compl_singleton x) isOpen_compl_singleton

Density Preservation under Singleton Removal in T₁ Spaces

Informal description

Let $X$ be a T₁ space, $s \subseteq X$ a dense subset, and $x \in X$ a point such that the punctured neighborhood filter $\mathcal{N}[X \setminus \{x\}]$ is non-trivial. Then the set $s \setminus \{x\}$ is dense in $X$.

Dense.diff_finset theorem

[T1Space X] [∀ x : X, NeBot (𝓝[≠] x)] {s : Set X} (hs : Dense s) (t : Finset X) : Dense (s \ t)

Full source

/-- Removing a finset from a dense set in a space without isolated points, one still
obtains a dense set. -/
theorem Dense.diff_finset [T1Space X] [∀ x : X, NeBot (𝓝[≠] x)] {s : Set X} (hs : Dense s)
    (t : Finset X) : Dense (s \ t) := by
  classical
  induction t using Finset.induction_on with
  | empty => simpa using hs
  | insert _ _ _ ih =>
    rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
    exact ih.diff_singleton _

Density Preservation under Finite Removal in T₁ Spaces

Informal description

Let $X$ be a T₁ space where for every point $x \in X$, the punctured neighborhood filter $\mathcal{N}[X \setminus \{x\}]$ is non-trivial. If $s \subseteq X$ is a dense subset and $t$ is a finite subset of $X$, then the set difference $s \setminus t$ is dense in $X$.

Dense.diff_finite theorem

[T1Space X] [∀ x : X, NeBot (𝓝[≠] x)] {s : Set X} (hs : Dense s) {t : Set X} (ht : t.Finite) : Dense (s \ t)

Full source

/-- Removing a finite set from a dense set in a space without isolated points, one still
obtains a dense set. -/
theorem Dense.diff_finite [T1Space X] [∀ x : X, NeBot (𝓝[≠] x)] {s : Set X} (hs : Dense s)
    {t : Set X} (ht : t.Finite) : Dense (s \ t) := by
  convert hs.diff_finset ht.toFinset
  exact (Finite.coe_toFinset _).symm

Density Preservation under Finite Removal in T₁ Spaces without Isolated Points

Informal description

Let $ X $ be a T₁ space where for every point $ x \in X $, the punctured neighborhood filter at $ x $ (i.e., the filter of neighborhoods of $ x $ excluding $ x $ itself) is non-trivial. If $ s \subseteq X $ is a dense subset and $ t \subseteq X $ is a finite subset, then the set difference $ s \setminus t $ is dense in $ X $.

Filter.Tendsto.eventually_ne theorem

 {X} [TopologicalSpace Y] [T1Space Y] {g : X → Y} {l : Filter X} {b₁ b₂ : Y} (hg : Tendsto g l (𝓝 b₁)) (hb : b₁ ≠ b₂) :
  ∀ᶠ z in l, g z ≠ b₂

Full source

theorem Filter.Tendsto.eventually_ne {X} [TopologicalSpace Y] [T1Space Y] {g : X → Y}
    {l : Filter X} {b₁ b₂ : Y} (hg : Tendsto g l (𝓝 b₁)) (hb : b₁ ≠ b₂) : ∀ᶠ z in l, g z ≠ b₂ :=
  hg.eventually (isOpen_compl_singleton.eventually_mem hb)

Eventual Distinctness of Limit Points in T₁ Spaces

Informal description

Let $ X $ and $ Y $ be topological spaces with $ Y $ a T₁ space. Let $ g : X \to Y $ be a function, $ l $ a filter on $ X $, and $ b₁, b₂ \in Y $ distinct points. If $ g $ tends to $ b₁ $ along $ l $, then for eventually all $ z $ in $ l $, $ g(z) \neq b₂ $.

ContinuousAt.eventually_ne theorem

 [TopologicalSpace Y] [T1Space Y] {g : X → Y} {x : X} {y : Y} (hg1 : ContinuousAt g x) (hg2 : g x ≠ y) :
  ∀ᶠ z in 𝓝 x, g z ≠ y

Full source

theorem ContinuousAt.eventually_ne [TopologicalSpace Y] [T1Space Y] {g : X → Y} {x : X} {y : Y}
    (hg1 : ContinuousAt g x) (hg2 : g x ≠ y) : ∀ᶠ z in 𝓝 x, g z ≠ y :=
  hg1.tendsto.eventually_ne hg2

Eventual Distinctness under Continuous Maps in T₁ Spaces

Informal description

Let $ X $ and $ Y $ be topological spaces with $ Y $ a T₁ space. Let $ g : X \to Y $ be a function that is continuous at a point $ x \in X $, and let $ y \in Y $ be distinct from $ g(x) $. Then, for all points $ z $ in some neighborhood of $ x $, $ g(z) \neq y $.

eventually_ne_nhds theorem

[T1Space X] {a b : X} (h : a ≠ b) : ∀ᶠ x in 𝓝 a, x ≠ b

Full source

theorem eventually_ne_nhds [T1Space X] {a b : X} (h : a ≠ b) : ∀ᶠ x in 𝓝 a, x ≠ b :=
  IsOpen.eventually_mem isOpen_ne h

Neighborhood Separation of Distinct Points in T₁ Spaces

Informal description

In a T₁ space $X$, for any two distinct points $a \neq b$, there exists a neighborhood of $a$ such that all points $x$ in this neighborhood satisfy $x \neq b$.

eventually_ne_nhdsWithin theorem

[T1Space X] {a b : X} {s : Set X} (h : a ≠ b) : ∀ᶠ x in 𝓝[s] a, x ≠ b

Full source

theorem eventually_ne_nhdsWithin [T1Space X] {a b : X} {s : Set X} (h : a ≠ b) :
    ∀ᶠ x in 𝓝[s] a, x ≠ b :=
  Filter.Eventually.filter_mono nhdsWithin_le_nhds <| eventually_ne_nhds h

Neighborhood Separation of Distinct Points within a Subset in T₁ Spaces

Informal description

Let $X$ be a T₁ space, and let $a, b \in X$ be distinct points. For any subset $s \subseteq X$, there exists a neighborhood of $a$ within $s$ such that all points $x$ in this neighborhood satisfy $x \neq b$.

continuousWithinAt_insert theorem

 [TopologicalSpace Y] [T1Space X] {x y : X} {s : Set X} {f : X → Y} :
  ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x

Full source

theorem continuousWithinAt_insert [TopologicalSpace Y] [T1Space X]
    {x y : X} {s : Set X} {f : X → Y} :
    ContinuousWithinAtContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x := by
  rcases eq_or_ne x y with (rfl | h)
  · exact continuousWithinAt_insert_self
  simp_rw [ContinuousWithinAt, nhdsWithin_insert_of_ne h]

Continuity within a Set with Inserted Point in T₁ Spaces

Informal description

Let $X$ be a T₁ space and $Y$ a topological space. For any function $f \colon X \to Y$, distinct points $x, y \in X$, and subset $s \subseteq X$, the function $f$ is continuous within the set $\{y\} \cup s$ at $x$ if and only if it is continuous within $s$ at $x$.

continuousWithinAt_diff_singleton theorem

 [TopologicalSpace Y] [T1Space X] {x y : X} {s : Set X} {f : X → Y} :
  ContinuousWithinAt f (s \ { y }) x ↔ ContinuousWithinAt f s x

Full source

/-- See also `continuousWithinAt_diff_self` for the case `y = x` but not requiring `T1Space`. -/
theorem continuousWithinAt_diff_singleton [TopologicalSpace Y] [T1Space X]
    {x y : X} {s : Set X} {f : X → Y} :
    ContinuousWithinAtContinuousWithinAt f (s \ {y}) x ↔ ContinuousWithinAt f s x := by
  rw [← continuousWithinAt_insert, insert_diff_singleton, continuousWithinAt_insert]

Continuity within a Set Minus a Point in T₁ Spaces

Informal description

Let $X$ be a T₁ space and $Y$ a topological space. For any function $f \colon X \to Y$, distinct points $x, y \in X$, and subset $s \subseteq X$, the function $f$ is continuous within the set $s \setminus \{y\}$ at $x$ if and only if it is continuous within $s$ at $x$.

continuousWithinAt_congr_set' theorem

 [TopologicalSpace Y] [T1Space X] {x : X} {s t : Set X} {f : X → Y} (y : X) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
  ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

Full source

/-- If two sets coincide locally around `x`, except maybe at `y`, then it is equivalent to be
continuous at `x` within one set or the other. -/
theorem continuousWithinAt_congr_set' [TopologicalSpace Y] [T1Space X]
    {x : X} {s t : Set X} {f : X → Y} (y : X) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
    ContinuousWithinAtContinuousWithinAt f s x ↔ ContinuousWithinAt f t x := by
  rw [← continuousWithinAt_insert_self (s := s), ← continuousWithinAt_insert_self (s := t)]
  exact continuousWithinAt_congr_set (eventuallyEq_insert h)

Equivalence of Continuity within Sets that Coincide Locally Except at One Point in T₁ Spaces

Informal description

Let $X$ be a T₁ space and $Y$ a topological space. For a function $f \colon X \to Y$, a point $x \in X$, and subsets $s, t \subseteq X$, suppose there exists a point $y \in X$ such that $s$ and $t$ coincide in a neighborhood of $x$ excluding $y$ (i.e., $s = t$ for all points sufficiently close to $x$ except possibly $y$). Then $f$ is continuous within $s$ at $x$ if and only if it is continuous within $t$ at $x$.

continuousAt_of_tendsto_nhds theorem

[TopologicalSpace Y] [T1Space Y] {f : X → Y} {x : X} {y : Y} (h : Tendsto f (𝓝 x) (𝓝 y)) : ContinuousAt f x

Full source

/-- To prove a function to a `T1Space` is continuous at some point `x`, it suffices to prove that
`f` admits *some* limit at `x`. -/
theorem continuousAt_of_tendsto_nhds [TopologicalSpace Y] [T1Space Y] {f : X → Y} {x : X} {y : Y}
    (h : Tendsto f (𝓝 x) (𝓝 y)) : ContinuousAt f x := by
  rwa [ContinuousAt, eq_of_tendsto_nhds h]

Continuity from Limit in T₁ Spaces

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ a T₁ space. For a function $f : X \to Y$, a point $x \in X$, and $y \in Y$, if the limit of $f$ at $x$ is $y$ (i.e., $f$ tends to $y$ as the input approaches $x$), then $f$ is continuous at $x$.

tendsto_const_nhds_iff theorem

[T1Space X] {l : Filter Y} [NeBot l] {c d : X} : Tendsto (fun _ => c) l (𝓝 d) ↔ c = d

Full source

@[simp]
theorem tendsto_const_nhds_iff [T1Space X] {l : Filter Y} [NeBot l] {c d : X} :
    TendstoTendsto (fun _ => c) l (𝓝 d) ↔ c = d := by simp_rw [Tendsto, Filter.map_const, pure_le_nhds_iff]

Characterization of Constant Function Limits in T₁ Spaces: $\lim_{l} (x \mapsto c) = d \leftrightarrow c = d$

Informal description

Let $X$ be a T₁ space and $Y$ a topological space with a non-trivial filter $l$ on $Y$. For any two points $c, d \in X$, the constant function mapping every element of $Y$ to $c$ tends to $d$ along $l$ if and only if $c = d$.

isOpen_singleton_of_finite_mem_nhds theorem

[T1Space X] (x : X) {s : Set X} (hs : s ∈ 𝓝 x) (hsf : s.Finite) : IsOpen ({ x } : Set X)

Full source

/-- A point with a finite neighborhood has to be isolated. -/
theorem isOpen_singleton_of_finite_mem_nhds [T1Space X] (x : X)
    {s : Set X} (hs : s ∈ 𝓝 x) (hsf : s.Finite) : IsOpen ({x} : Set X) := by
  have A : {x}{x} ⊆ s := by simp only [singleton_subset_iff, mem_of_mem_nhds hs]
  have B : IsClosed (s \ {x}) := (hsf.subset diff_subset).isClosed
  have C : (s \ {x})ᶜ(s \ {x})ᶜ ∈ 𝓝 x := B.isOpen_compl.mem_nhds fun h => h.2 rfl
  have D : {x}{x} ∈ 𝓝 x := by simpa only [← diff_eq, diff_diff_cancel_left A] using inter_mem hs C
  rwa [← mem_interior_iff_mem_nhds, ← singleton_subset_iff, subset_interior_iff_isOpen] at D

Openness of Singleton in T₁ Space with Finite Neighborhood

Informal description

Let $ X $ be a T₁ space and $ x \in X $. If there exists a finite neighborhood $ s $ of $ x $ (i.e., $ s $ is a finite set containing $ x $ and $ s $ is a neighborhood of $ x $), then the singleton set $\{x\}$ is open in $ X $.

infinite_of_mem_nhds theorem

 {X} [TopologicalSpace X] [T1Space X] (x : X) [hx : NeBot (𝓝[≠] x)] {s : Set X} (hs : s ∈ 𝓝 x) : Set.Infinite s

Full source

/-- If the punctured neighborhoods of a point form a nontrivial filter, then any neighborhood is
infinite. -/
theorem infinite_of_mem_nhds {X} [TopologicalSpace X] [T1Space X] (x : X) [hx : NeBot (𝓝[≠] x)]
    {s : Set X} (hs : s ∈ 𝓝 x) : Set.Infinite s := by
  refine fun hsf => hx.1 ?_
  rw [← isOpen_singleton_iff_punctured_nhds]
  exact isOpen_singleton_of_finite_mem_nhds x hs hsf

Infinite Neighborhoods in T₁ Spaces with Nontrivial Punctured Filters

Informal description

Let $X$ be a T₁ space and $x \in X$. If the punctured neighborhood filter $\mathcal{N}_x \setminus \{x\}$ is nontrivial (i.e., it does not contain the empty set), then any neighborhood $s$ of $x$ is infinite.

Finite.instDiscreteTopology instance

[T1Space X] [Finite X] : DiscreteTopology X

Full source

instance Finite.instDiscreteTopology [T1Space X] [Finite X] : DiscreteTopology X :=
  discreteTopology_iff_forall_isClosed.mpr (· |>.toFinite.isClosed)

Finite T₁ Spaces are Discrete

Informal description

Every finite T₁ space $X$ has the discrete topology.

Set.Finite.continuousOn theorem

[T1Space X] [TopologicalSpace Y] {s : Set X} (hs : s.Finite) (f : X → Y) : ContinuousOn f s

Full source

theorem Set.Finite.continuousOn [T1Space X] [TopologicalSpace Y] {s : Set X} (hs : s.Finite)
    (f : X → Y) : ContinuousOn f s := by
  rw [continuousOn_iff_continuous_restrict]
  have : Finite s := hs
  fun_prop

Continuity of Functions on Finite Subsets of T₁ Spaces

Informal description

Let $X$ be a T₁ space and $Y$ a topological space. For any finite subset $s \subseteq X$ and any function $f : X \to Y$, the restriction of $f$ to $s$ is continuous.

SeparationQuotient.t1Space_iff theorem

: T1Space (SeparationQuotient X) ↔ R0Space X

Full source

theorem SeparationQuotient.t1Space_iff : T1SpaceT1Space (SeparationQuotient X) ↔ R0Space X := by
  rw [r0Space_iff, ((t1Space_TFAE (SeparationQuotient X)).out 0 9 :)]
  constructor
  · intro h x y xspecy
    rw [← IsInducing.specializes_iff isInducing_mk, h xspecy] at *
  · -- TODO is there are better way to do this,
    -- so the case split produces `SeparationQuotient.mk` directly, rather than `Quot.mk`?
    -- Currently we need the `change` statement to recover this.
    rintro h ⟨x⟩ ⟨y⟩ sxspecsy
    change mk _ = mk _
    have xspecy : x ⤳ y := isInducing_mk.specializes_iff.mp sxspecsy
    have yspecx : y ⤳ x := h xspecy
    rw [mk_eq_mk, inseparable_iff_specializes_and]
    exact ⟨xspecy, yspecx⟩

T₁ Property of Separation Quotient Equivalent to R₀ Property of Original Space

Informal description

The separation quotient of a topological space $X$ is a T₁ space if and only if $X$ is an R₀ space.

isClosed_inter_singleton theorem

[T1Space X] {A : Set X} {a : X} : IsClosed (A ∩ { a })

Full source

lemma isClosed_inter_singleton [T1Space X] {A : Set X} {a : X} : IsClosed (A ∩ {a}) :=
  Subsingleton.inter_singleton.isClosed

Closedness of Intersection with Singleton in T₁ Space

Informal description

In a T₁ space $X$, for any subset $A \subseteq X$ and any point $a \in X$, the intersection $A \cap \{a\}$ is closed in $X$.

isClosed_singleton_inter theorem

[T1Space X] {A : Set X} {a : X} : IsClosed ({ a } ∩ A)

Full source

lemma isClosed_singleton_inter [T1Space X] {A : Set X} {a : X} : IsClosed ({a}{a} ∩ A) :=
  Subsingleton.singleton_inter.isClosed

Closedness of Singleton Intersection in T₁ Space

Informal description

In a T₁ space $X$, for any subset $A \subseteq X$ and any point $a \in X$, the intersection $\{a\} \cap A$ is closed in $X$.

singleton_mem_nhdsWithin_of_mem_discrete theorem

{s : Set X} [DiscreteTopology s] {x : X} (hx : x ∈ s) : { x } ∈ 𝓝[s] x

Full source

theorem singleton_mem_nhdsWithin_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X}
    (hx : x ∈ s) : {x}{x} ∈ 𝓝[s] x := by
  have : ({⟨x, hx⟩} : Set s) ∈ 𝓝 (⟨x, hx⟩ : s) := by simp [nhds_discrete]
  simpa only [nhdsWithin_eq_map_subtype_coe hx, image_singleton] using
    @image_mem_map _ _ _ ((↑) : s → X) _ this

Singleton Neighborhood in Discrete Subspace

Informal description

Let $X$ be a topological space and $s \subseteq X$ a subset with the discrete topology. For any point $x \in s$, the singleton set $\{x\}$ is a neighborhood of $x$ in the subspace topology of $s$.

nhdsWithin_of_mem_discrete theorem

{s : Set X} [DiscreteTopology s] {x : X} (hx : x ∈ s) : 𝓝[s] x = pure x

Full source

/-- The neighbourhoods filter of `x` within `s`, under the discrete topology, is equal to
the pure `x` filter (which is the principal filter at the singleton `{x}`.) -/
theorem nhdsWithin_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X} (hx : x ∈ s) :
    𝓝[s] x = pure x :=
  le_antisymm (le_pure_iff.2 <| singleton_mem_nhdsWithin_of_mem_discrete hx) (pure_le_nhdsWithin hx)

Neighborhood Filter in Discrete Subspace Equals Singleton Filter

Informal description

Let $X$ be a topological space and $s \subseteq X$ a subset with the discrete topology. For any point $x \in s$, the neighborhood filter of $x$ within $s$ is equal to the principal filter generated by $\{x\}$ (i.e., $\mathcal{N}_s(x) = \{\{x\}\}$).

Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete theorem

 {ι : Type*} {p : ι → Prop} {t : ι → Set X} {s : Set X} [DiscreteTopology s] {x : X} (hb : (𝓝 x).HasBasis p t)
  (hx : x ∈ s) : ∃ i, p i ∧ t i ∩ s = { x }

Full source

theorem Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete {ι : Type*} {p : ι → Prop}
    {t : ι → Set X} {s : Set X} [DiscreteTopology s] {x : X} (hb : (𝓝 x).HasBasis p t)
    (hx : x ∈ s) : ∃ i, p i ∧ t i ∩ s = {x} := by
  rcases (nhdsWithin_hasBasis hb s).mem_iff.1 (singleton_mem_nhdsWithin_of_mem_discrete hx) with
    ⟨i, hi, hix⟩
  exact ⟨i, hi, hix.antisymm <| singleton_subset_iff.2 ⟨mem_of_mem_nhds <| hb.mem_of_mem hi, hx⟩⟩

Existence of Neighborhood Basis Element Yielding Singleton Intersection in Discrete Subspace

Informal description

Let $X$ be a topological space and $s \subseteq X$ a subset with the discrete topology. Suppose the neighborhood filter $\mathcal{N}(x)$ of a point $x \in s$ has a basis $\{t_i\}_{i \in \iota}$ indexed by some type $\iota$ with a predicate $p : \iota \to \text{Prop}$. Then there exists an index $i \in \iota$ such that $p(i)$ holds and the intersection $t_i \cap s$ is exactly the singleton set $\{x\}$.

nhds_inter_eq_singleton_of_mem_discrete theorem

{s : Set X} [DiscreteTopology s] {x : X} (hx : x ∈ s) : ∃ U ∈ 𝓝 x, U ∩ s = { x }

Full source

/-- A point `x` in a discrete subset `s` of a topological space admits a neighbourhood
that only meets `s` at `x`. -/
theorem nhds_inter_eq_singleton_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X}
    (hx : x ∈ s) : ∃ U ∈ 𝓝 x, U ∩ s = {x} := by
  simpa using (𝓝 x).basis_sets.exists_inter_eq_singleton_of_mem_discrete hx

Existence of Neighborhood with Singleton Intersection in Discrete Subspace

Informal description

Let $X$ be a topological space and $s \subseteq X$ a subset with the discrete topology. For any point $x \in s$, there exists a neighborhood $U$ of $x$ in $X$ such that the intersection $U \cap s$ is exactly the singleton set $\{x\}$.

isOpen_inter_eq_singleton_of_mem_discrete theorem

{s : Set X} [DiscreteTopology s] {x : X} (hx : x ∈ s) : ∃ U : Set X, IsOpen U ∧ U ∩ s = { x }

Full source

/-- Let `x` be a point in a discrete subset `s` of a topological space, then there exists an open
set that only meets `s` at `x`. -/
theorem isOpen_inter_eq_singleton_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X}
    (hx : x ∈ s) : ∃ U : Set X, IsOpen U ∧ U ∩ s = {x} := by
  obtain ⟨U, hU_nhds, hU_inter⟩ := nhds_inter_eq_singleton_of_mem_discrete hx
  obtain ⟨t, ht_sub, ht_open, ht_x⟩ := mem_nhds_iff.mp hU_nhds
  refine ⟨t, ht_open, Set.Subset.antisymm ?_ ?_⟩
  · exact hU_inter ▸ Set.inter_subset_inter_left s ht_sub
  · rw [Set.subset_inter_iff, Set.singleton_subset_iff, Set.singleton_subset_iff]
    exact ⟨ht_x, hx⟩

Existence of Open Neighborhood with Singleton Intersection in Discrete Subspace

Informal description

Let $X$ be a topological space and $s \subseteq X$ a subset with the discrete topology. For any point $x \in s$, there exists an open set $U \subseteq X$ such that $U \cap s = \{x\}$.

disjoint_nhdsWithin_of_mem_discrete theorem

{s : Set X} [DiscreteTopology s] {x : X} (hx : x ∈ s) : ∃ U ∈ 𝓝[≠] x, Disjoint U s

Full source

/-- For point `x` in a discrete subset `s` of a topological space, there is a set `U`
such that
1. `U` is a punctured neighborhood of `x` (ie. `U ∪ {x}` is a neighbourhood of `x`),
2. `U` is disjoint from `s`.
-/
theorem disjoint_nhdsWithin_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X} (hx : x ∈ s) :
    ∃ U ∈ 𝓝[≠] x, Disjoint U s :=
  let ⟨V, h, h'⟩ := nhds_inter_eq_singleton_of_mem_discrete hx
  ⟨{x}ᶜ ∩ V, inter_mem_nhdsWithin _ h,
    disjoint_iff_inter_eq_empty.mpr (by rw [inter_assoc, h', compl_inter_self])⟩

Existence of Punctured Neighborhood Disjoint from Discrete Subset

Informal description

Let $X$ be a topological space and $s \subseteq X$ a subset with the discrete topology. For any point $x \in s$, there exists a punctured neighborhood $U$ of $x$ (i.e., $U \cup \{x\}$ is a neighborhood of $x$) such that $U$ is disjoint from $s$.

isClosedEmbedding_update theorem

 {ι : Type*} {β : ι → Type*} [DecidableEq ι] [(i : ι) → TopologicalSpace (β i)] (x : (i : ι) → β i) (i : ι)
  [(i : ι) → T1Space (β i)] : IsClosedEmbedding (update x i)

Full source

theorem isClosedEmbedding_update {ι : Type*} {β : ι → Type*}
    [DecidableEq ι] [(i : ι) → TopologicalSpace (β i)]
    (x : (i : ι) → β i) (i : ι) [(i : ι) → T1Space (β i)] :
    IsClosedEmbedding (update x i) := by
  refine .of_continuous_injective_isClosedMap (continuous_const.update i continuous_id)
    (update_injective x i) fun s hs ↦ ?_
  rw [update_image]
  apply isClosed_set_pi
  simp [forall_update_iff, hs, isClosed_singleton]

Function Update is a Closed Embedding in Product of T₁ Spaces

Informal description

Let $\{β_i\}_{i \in \iota}$ be a family of topological spaces indexed by a type $\iota$ with decidable equality, where each $β_i$ is a T₁ space. For any point $x \in \prod_{i \in \iota} β_i$ and any index $i \in \iota$, the function update operation $\text{update } x \, i : β_i \to \prod_{i \in \iota} β_i$ (which replaces the $i$-th coordinate of $x$ with a given value) is a closed embedding.

R1Space structure

(X : Type*) [TopologicalSpace X]

Full source

/-- A topological space is called a *preregular* (a.k.a. R₁) space,
if any two topologically distinguishable points have disjoint neighbourhoods. -/
@[mk_iff r1Space_iff_specializes_or_disjoint_nhds]
class R1Space (X : Type*) [TopologicalSpace X] : Prop where
  specializes_or_disjoint_nhds (x y : X) : SpecializesSpecializes x y ∨ Disjoint (𝓝 x) (𝓝 y)

Preregular (R₁) Space

Informal description

A topological space $ X $ is called a *preregular* (or R₁) space if any two topologically distinguishable points in $ X $ have disjoint neighborhoods. This means that for any two points $ x $ and $ y $ in $ X $ that are topologically distinguishable (i.e., there exists an open set containing one but not the other), there exist open neighborhoods $ U $ of $ x $ and $ V $ of $ y $ such that $ U $ and $ V $ are disjoint.

instR0Space instance

: R0Space X

Full source

instance (priority := 100) : R0Space X where
  specializes_symmetric _ _ h := (specializes_or_disjoint_nhds _ _).resolve_right <| fun hd ↦
    h.not_disjoint hd.symm

Preregular Spaces are R₀ Spaces

Informal description

Every preregular (R₁) space is an R₀ space.

disjoint_nhds_nhds_iff_not_specializes theorem

: Disjoint (𝓝 x) (𝓝 y) ↔ ¬x ⤳ y

Full source

theorem disjoint_nhds_nhds_iff_not_specializes : DisjointDisjoint (𝓝 x) (𝓝 y) ↔ ¬x ⤳ y :=
  ⟨fun hd hspec ↦ hspec.not_disjoint hd, (specializes_or_disjoint_nhds _ _).resolve_left⟩

Disjoint Neighborhoods and Specialization Relation: $\text{Disjoint}(\mathcal{N}(x), \mathcal{N}(y)) \leftrightarrow \neg (x \leadsto y)$

Informal description

For any two points $x$ and $y$ in a topological space, the neighborhoods of $x$ and $y$ are disjoint if and only if $x$ does not specialize to $y$. In other words, $\text{Disjoint}(\mathcal{N}(x), \mathcal{N}(y)) \leftrightarrow \neg (x \leadsto y)$, where $\mathcal{N}(x)$ denotes the neighborhood filter at $x$ and $\leadsto$ denotes the specialization relation.

specializes_iff_not_disjoint theorem

: x ⤳ y ↔ ¬Disjoint (𝓝 x) (𝓝 y)

Full source

theorem specializes_iff_not_disjoint : x ⤳ yx ⤳ y ↔ ¬Disjoint (𝓝 x) (𝓝 y) :=
  disjoint_nhds_nhds_iff_not_specializes.not_left.symm

Specialization Relation and Neighborhood Disjointness: $x \leadsto y \leftrightarrow \neg \text{Disjoint}(\mathcal{N}(x), \mathcal{N}(y))$

Informal description

For any two points $x$ and $y$ in a topological space, $x$ specializes to $y$ if and only if the neighborhoods of $x$ and $y$ are not disjoint, i.e., $x \leadsto y \leftrightarrow \neg \text{Disjoint}(\mathcal{N}(x), \mathcal{N}(y))$.

disjoint_nhds_nhds_iff_not_inseparable theorem

: Disjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y

Full source

theorem disjoint_nhds_nhds_iff_not_inseparable : DisjointDisjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y := by
  rw [disjoint_nhds_nhds_iff_not_specializes, specializes_iff_inseparable]

Disjoint Neighborhoods and Inseparability: $\text{Disjoint}(\mathcal{N}(x), \mathcal{N}(y)) \leftrightarrow \neg (\text{Inseparable}(x, y))$

Informal description

For any two points $x$ and $y$ in a topological space, the neighborhoods $\mathcal{N}(x)$ and $\mathcal{N}(y)$ are disjoint if and only if $x$ and $y$ are topologically inseparable, i.e., $\text{Disjoint}(\mathcal{N}(x), \mathcal{N}(y)) \leftrightarrow \neg (\text{Inseparable}(x, y))$.

r1Space_iff_inseparable_or_disjoint_nhds theorem

{X : Type*} [TopologicalSpace X] : R1Space X ↔ ∀ x y : X, Inseparable x y ∨ Disjoint (𝓝 x) (𝓝 y)

Full source

theorem r1Space_iff_inseparable_or_disjoint_nhds {X : Type*} [TopologicalSpace X] :
    R1SpaceR1Space X ↔ ∀ x y : X, Inseparable x y ∨ Disjoint (𝓝 x) (𝓝 y) :=
  ⟨fun _h x y ↦ (specializes_or_disjoint_nhds x y).imp_left Specializes.inseparable, fun h ↦
    ⟨fun x y ↦ (h x y).imp_left Inseparable.specializes⟩⟩

Characterization of Preregular (R₁) Spaces via Inseparability or Disjoint Neighborhoods

Informal description

A topological space $ X $ is a preregular (R₁) space if and only if for any two points $ x $ and $ y $ in $ X $, either $ x $ and $ y $ are topologically inseparable or their neighborhoods are disjoint. In other words, $ X $ is R₁ precisely when for all $ x, y \in X $, either $ \text{Inseparable}(x, y) $ holds or there exist disjoint open neighborhoods $ U $ of $ x $ and $ V $ of $ y $.

Inseparable.of_nhds_neBot theorem

{x y : X} (h : NeBot (𝓝 x ⊓ 𝓝 y)) : Inseparable x y

Full source

theorem Inseparable.of_nhds_neBot {x y : X} (h : NeBot (𝓝𝓝 x ⊓ 𝓝 y)) :
    Inseparable x y :=
  (r1Space_iff_inseparable_or_disjoint_nhds.mp ‹_› _ _).resolve_right fun h' => h.ne h'.eq_bot

Non-trivial Neighborhood Intersection Implies Inseparability

Informal description

For any two points $x$ and $y$ in a topological space $X$, if the intersection of their neighborhoods $\mathcal{N}(x) \sqcap \mathcal{N}(y)$ is non-trivial (i.e., not the trivial filter), then $x$ and $y$ are topologically inseparable.

r1_separation theorem

{x y : X} (h : ¬Inseparable x y) : ∃ u v : Set X, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Full source

theorem r1_separation {x y : X} (h : ¬Inseparable x y) :
    ∃ u v : Set X, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v := by
  rw [← disjoint_nhds_nhds_iff_not_inseparable,
    (nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)] at h
  obtain ⟨u, ⟨hxu, hu⟩, v, ⟨hyv, hv⟩, huv⟩ := h
  exact ⟨u, v, hu, hv, hxu, hyv, huv⟩

Existence of Disjoint Neighborhoods for Topologically Distinguishable Points in R₁ Spaces

Informal description

For any two points $x$ and $y$ in a preregular (R₁) topological space $X$, if $x$ and $y$ are topologically distinguishable (i.e., $\neg \text{Inseparable}(x, y)$), then there exist disjoint open neighborhoods $U$ of $x$ and $V$ of $y$ such that $x \in U$, $y \in V$, and $U \cap V = \emptyset$.

tendsto_nhds_unique_inseparable theorem

 {f : Y → X} {l : Filter Y} {a b : X} [NeBot l] (ha : Tendsto f l (𝓝 a)) (hb : Tendsto f l (𝓝 b)) : Inseparable a b

Full source

/-- Limits are unique up to separability.

A weaker version of `tendsto_nhds_unique` for `R1Space`. -/
theorem tendsto_nhds_unique_inseparable {f : Y → X} {l : Filter Y} {a b : X} [NeBot l]
    (ha : Tendsto f l (𝓝 a)) (hb : Tendsto f l (𝓝 b)) : Inseparable a b :=
  .of_nhds_neBot <| neBot_of_le <| le_inf ha hb

Uniqueness of Limits in Preregular Spaces up to Inseparability

Informal description

Let $X$ be a preregular (R₁) topological space, $Y$ a topological space, and $f: Y \to X$ a function. For any filter $l$ on $Y$ that is not the trivial filter, if $f$ tends to both $a$ and $b$ in $X$ along $l$, then $a$ and $b$ are topologically inseparable points in $X$.

isClosed_setOf_specializes theorem

: IsClosed {p : X × X | p.1 ⤳ p.2}

Full source

theorem isClosed_setOf_specializes : IsClosed { p : X × X | p.1 ⤳ p.2 } := by
  simp only [← isOpen_compl_iff, compl_setOf, ← disjoint_nhds_nhds_iff_not_specializes,
    isOpen_setOf_disjoint_nhds_nhds]

Closedness of the Specialization Relation in Product Space

Informal description

In a topological space $X$, the set $\{(x, y) \in X \times X \mid x \text{ specializes to } y\}$ is closed in the product topology of $X \times X$.

isClosed_setOf_inseparable theorem

: IsClosed {p : X × X | Inseparable p.1 p.2}

Full source

theorem isClosed_setOf_inseparable : IsClosed { p : X × X | Inseparable p.1 p.2 } := by
  simp only [← specializes_iff_inseparable, isClosed_setOf_specializes]

Closedness of the Inseparability Relation in Product Space

Informal description

In a topological space $X$, the set $\{(x, y) \in X \times X \mid x \text{ and } y \text{ are inseparable}\}$ is closed in the product topology of $X \times X$.

IsCompact.mem_closure_iff_exists_inseparable theorem

{K : Set X} (hK : IsCompact K) : y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y

Full source

/-- In an R₁ space, a point belongs to the closure of a compact set `K`
if and only if it is topologically inseparable from some point of `K`. -/
theorem IsCompact.mem_closure_iff_exists_inseparable {K : Set X} (hK : IsCompact K) :
    y ∈ closure Ky ∈ closure K ↔ ∃ x ∈ K, Inseparable x y := by
  refine ⟨fun hy ↦ ?_, fun ⟨x, hxK, hxy⟩ ↦
    (hxy.mem_closed_iff isClosed_closure).1 <| subset_closure hxK⟩
  contrapose! hy
  have : Disjoint (𝓝 y) (𝓝ˢ K) := hK.disjoint_nhdsSet_right.2 fun x hx ↦
    (disjoint_nhds_nhds_iff_not_inseparable.2 (hy x hx)).symm
  simpa only [disjoint_iff, not_mem_closure_iff_nhdsWithin_eq_bot]
    using this.mono_right principal_le_nhdsSet

Characterization of Closure Points in Compact Sets via Inseparability in R₁ Spaces

Informal description

Let $X$ be an R₁ space and $K \subseteq X$ a compact subset. A point $y \in X$ belongs to the closure of $K$ if and only if there exists a point $x \in K$ such that $x$ and $y$ are topologically inseparable (i.e., they share the same neighborhood filter).

IsCompact.closure_eq_biUnion_inseparable theorem

{K : Set X} (hK : IsCompact K) : closure K = ⋃ x ∈ K, {y | Inseparable x y}

Full source

theorem IsCompact.closure_eq_biUnion_inseparable {K : Set X} (hK : IsCompact K) :
    closure K = ⋃ x ∈ K, {y | Inseparable x y} := by
  ext; simp [hK.mem_closure_iff_exists_inseparable]

Closure of Compact Set as Union of Inseparable Points

Informal description

Let $X$ be a topological space and $K \subseteq X$ a compact subset. The closure of $K$ equals the union of all points in $K$ together with their inseparable points, i.e., \[ \overline{K} = \bigcup_{x \in K} \{ y \in X \mid x \text{ and } y \text{ are inseparable} \}. \]

IsCompact.closure_eq_biUnion_closure_singleton theorem

{K : Set X} (hK : IsCompact K) : closure K = ⋃ x ∈ K, closure { x }

Full source

/-- In an R₁ space, the closure of a compact set is the union of the closures of its points. -/
theorem IsCompact.closure_eq_biUnion_closure_singleton {K : Set X} (hK : IsCompact K) :
    closure K = ⋃ x ∈ K, closure {x} := by
  simp only [hK.closure_eq_biUnion_inseparable, ← specializes_iff_inseparable,
    specializes_iff_mem_closure, setOf_mem_eq]

Closure of Compact Set as Union of Singleton Closures

Informal description

Let $X$ be a topological space and $K \subseteq X$ a compact subset. The closure of $K$ equals the union of the closures of all singletons $\{x\}$ for $x \in K$, i.e., \[ \overline{K} = \bigcup_{x \in K} \overline{\{x\}}. \]

IsCompact.closure_subset_of_isOpen theorem

{K : Set X} (hK : IsCompact K) {U : Set X} (hU : IsOpen U) (hKU : K ⊆ U) : closure K ⊆ U

Full source

/-- In an R₁ space, if a compact set `K` is contained in an open set `U`,
then its closure is also contained in `U`. -/
theorem IsCompact.closure_subset_of_isOpen {K : Set X} (hK : IsCompact K)
    {U : Set X} (hU : IsOpen U) (hKU : K ⊆ U) : closureclosure K ⊆ U := by
  rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]
  exact fun x hx y hxy ↦ (hxy.mem_open_iff hU).1 (hKU hx)

Closure of Compact Set in R₁ Space is Contained in Open Superset

Informal description

Let $ X $ be an R₁ space, $ K \subseteq X $ a compact subset, and $ U \subseteq X $ an open set such that $ K \subseteq U $. Then the closure of $ K $ is also contained in $ U $, i.e., $ \overline{K} \subseteq U $.

IsCompact.closure theorem

{K : Set X} (hK : IsCompact K) : IsCompact (closure K)

Full source

/-- The closure of a compact set in an R₁ space is a compact set. -/
protected theorem IsCompact.closure {K : Set X} (hK : IsCompact K) : IsCompact (closure K) := by
  refine isCompact_of_finite_subcover fun U hUo hKU ↦ ?_
  rcases hK.elim_finite_subcover U hUo (subset_closure.trans hKU) with ⟨t, ht⟩
  exact ⟨t, hK.closure_subset_of_isOpen (isOpen_biUnion fun _ _ ↦ hUo _) ht⟩

Closure of Compact Set in R₁ Space is Compact

Informal description

Let $X$ be an R₁ space and $K \subseteq X$ a compact subset. Then the closure of $K$, denoted $\overline{K}$, is also compact.

IsCompact.closure_of_subset theorem

{s K : Set X} (hK : IsCompact K) (h : s ⊆ K) : IsCompact (closure s)

Full source

theorem IsCompact.closure_of_subset {s K : Set X} (hK : IsCompact K) (h : s ⊆ K) :
    IsCompact (closure s) :=
  hK.closure.of_isClosed_subset isClosed_closure (closure_mono h)

Closure of Subset of Compact Set in R₁ Space is Compact

Informal description

Let $ X $ be an R₁ space, $ K \subseteq X $ a compact subset, and $ s \subseteq K $ any subset. Then the closure of $ s $, denoted $ \overline{s} $, is compact.

exists_isCompact_superset_iff theorem

{s : Set X} : (∃ K, IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure s)

Full source

@[simp]
theorem exists_isCompact_superset_iff {s : Set X} :
    (∃ K, IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure s) :=
  ⟨fun ⟨_K, hK, hsK⟩ => hK.closure_of_subset hsK, fun h => ⟨closure s, h, subset_closure⟩⟩

Compact Superset Existence Criterion via Closure in R₁ Spaces

Informal description

For any subset $s$ of an R₁ space $X$, there exists a compact set $K$ containing $s$ if and only if the closure of $s$ is compact. In other words, $(\exists K, \text{IsCompact}(K) \land s \subseteq K) \leftrightarrow \text{IsCompact}(\overline{s})$.

SeparatedNhds.of_isCompact_isCompact_isClosed theorem

{K L : Set X} (hK : IsCompact K) (hL : IsCompact L) (h'L : IsClosed L) (hd : Disjoint K L) : SeparatedNhds K L

Full source

/-- If `K` and `L` are disjoint compact sets in an R₁ topological space
and `L` is also closed, then `K` and `L` have disjoint neighborhoods. -/
theorem SeparatedNhds.of_isCompact_isCompact_isClosed {K L : Set X} (hK : IsCompact K)
    (hL : IsCompact L) (h'L : IsClosed L) (hd : Disjoint K L) : SeparatedNhds K L := by
  simp_rw [separatedNhds_iff_disjoint, hK.disjoint_nhdsSet_left, hL.disjoint_nhdsSet_right,
    disjoint_nhds_nhds_iff_not_inseparable]
  intro x hx y hy h
  exact absurd ((h.mem_closed_iff h'L).2 hy) <| disjoint_left.1 hd hx

Disjoint Neighborhoods for Compact and Closed Sets in R₁ Spaces

Informal description

Let $ X $ be an R₁ topological space, and let $ K $ and $ L $ be disjoint subsets of $ X $. If $ K $ is compact, $ L $ is both compact and closed, then there exist disjoint open neighborhoods $ U $ of $ K $ and $ V $ of $ L $.

IsCompact.binary_compact_cover theorem

 {K U V : Set X} (hK : IsCompact K) (hU : IsOpen U) (hV : IsOpen V) (h2K : K ⊆ U ∪ V) :
  ∃ K₁ K₂ : Set X, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Full source

/-- If a compact set is covered by two open sets, then we can cover it by two compact subsets. -/
theorem IsCompact.binary_compact_cover {K U V : Set X}
    (hK : IsCompact K) (hU : IsOpen U) (hV : IsOpen V) (h2K : K ⊆ U ∪ V) :
    ∃ K₁ K₂ : Set X, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂ := by
  have hK' : IsCompact (closure K) := hK.closure
  have : SeparatedNhds (closureclosure K \ U) (closureclosure K \ V) := by
    apply SeparatedNhds.of_isCompact_isCompact_isClosed (hK'.diff hU) (hK'.diff hV)
      (isClosed_closure.sdiff hV)
    rw [disjoint_iff_inter_eq_empty, diff_inter_diff, diff_eq_empty]
    exact hK.closure_subset_of_isOpen (hU.union hV) h2K
  have : SeparatedNhds (K \ U) (K \ V) :=
    this.mono (diff_subset_diff_left (subset_closure)) (diff_subset_diff_left (subset_closure))
  rcases this with ⟨O₁, O₂, h1O₁, h1O₂, h2O₁, h2O₂, hO⟩
  exact ⟨K \ O₁, K \ O₂, hK.diff h1O₁, hK.diff h1O₂, diff_subset_comm.mp h2O₁,
    diff_subset_comm.mp h2O₂, by rw [← diff_inter, hO.inter_eq, diff_empty]⟩

Compact Cover by Two Open Sets Decomposes into Two Compact Subsets

Informal description

Let $X$ be a topological space, $K \subseteq X$ a compact set, and $U, V \subseteq X$ open sets such that $K \subseteq U \cup V$. Then there exist compact sets $K_1 \subseteq U$ and $K_2 \subseteq V$ such that $K = K_1 \cup K_2$.

IsCompact.finite_compact_cover theorem

 {s : Set X} (hs : IsCompact s) {ι : Type*} (t : Finset ι) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen (U i))
  (hsC : s ⊆ ⋃ i ∈ t, U i) : ∃ K : ι → Set X, (∀ i, IsCompact (K i)) ∧ (∀ i, K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i

Full source

/-- For every finite open cover `Uᵢ` of a compact set, there exists a compact cover `Kᵢ ⊆ Uᵢ`. -/
theorem IsCompact.finite_compact_cover {s : Set X} (hs : IsCompact s) {ι : Type*}
    (t : Finset ι) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i) :
    ∃ K : ι → Set X, (∀ i, IsCompact (K i)) ∧ (∀ i, K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i := by
  classical
  induction t using Finset.induction generalizing U s with
  | empty =>
    refine ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, ?_⟩
    simpa only [subset_empty_iff, Finset.not_mem_empty, iUnion_false, iUnion_empty] using hsC
  | insert x t hx ih =>
    simp only [Finset.set_biUnion_insert] at hsC
    simp only [Finset.forall_mem_insert] at hU
    have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi
    rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with
      ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩
    rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩
    refine ⟨update K x K₁, ?_, ?_, ?_⟩
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h1K₁]
      · simp only [update_of_ne hi, h1K]
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h2K₁]
      · simp only [update_of_ne hi, h2K]
    · simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K]

Existence of Compact Refinement for Finite Open Covers of Compact Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact set. Given a finite open cover $\{U_i\}_{i \in t}$ of $s$ (where $t$ is a finite index set), there exists a family of compact sets $\{K_i\}_{i \in t}$ such that for each $i \in t$, $K_i \subseteq U_i$, and $s = \bigcup_{i \in t} K_i$.

R1Space.of_continuous_specializes_imp theorem

[TopologicalSpace Y] {f : Y → X} (hc : Continuous f) (hspec : ∀ x y, f x ⤳ f y → x ⤳ y) : R1Space Y

Full source

theorem R1Space.of_continuous_specializes_imp [TopologicalSpace Y] {f : Y → X} (hc : Continuous f)
    (hspec : ∀ x y, f x ⤳ f y → x ⤳ y) : R1Space Y where
  specializes_or_disjoint_nhds x y := (specializes_or_disjoint_nhds (f x) (f y)).imp (hspec x y) <|
    ((hc.tendsto _).disjoint · (hc.tendsto _))

Continuous map preserving specialization implies R₁ space

Informal description

Let $Y$ be a topological space and $f: Y \to X$ a continuous map. If for any points $x, y \in Y$, the condition $f(x) \rightsquigarrow f(y)$ implies $x \rightsquigarrow y$, then $Y$ is an R₁ space.

Topology.IsInducing.r1Space theorem

[TopologicalSpace Y] {f : Y → X} (hf : IsInducing f) : R1Space Y

Full source

theorem Topology.IsInducing.r1Space [TopologicalSpace Y] {f : Y → X} (hf : IsInducing f) :
    R1Space Y := .of_continuous_specializes_imp hf.continuous fun _ _ ↦ hf.specializes_iff.1

Induced Topology Preserves R₁ Property

Informal description

Let $Y$ be a topological space and $f: Y \to X$ an inducing map (i.e., the topology on $Y$ is induced by $f$ from the topology on $X$). If $X$ is an R₁ space, then $Y$ is also an R₁ space.

R1Space.induced theorem

(f : Y → X) : @R1Space Y (.induced f ‹_›)

Full source

protected theorem R1Space.induced (f : Y → X) : @R1Space Y (.induced f ‹_›) :=
  @IsInducing.r1Space _ _ _ _ (.induced f _) f (.induced f)

Induced Topology of an R₁ Space is R₁

Informal description

Let $X$ be an R₁ space and $f : Y \to X$ be a function. Then the topological space on $Y$ induced by $f$ (i.e., the coarsest topology on $Y$ making $f$ continuous) is also an R₁ space.

instR1SpaceSubtype instance

(p : X → Prop) : R1Space (Subtype p)

Full source

instance (p : X → Prop) : R1Space (Subtype p) := .induced _

Subspace of an R₁ Space is R₁

Informal description

For any topological space $X$ and any predicate $p : X \to \mathrm{Prop}$, the subtype $\{x \in X \mid p(x)\}$ equipped with the subspace topology is an R₁ space.

R1Space.sInf theorem

{X : Type*} {T : Set (TopologicalSpace X)} (hT : ∀ t ∈ T, @R1Space X t) : @R1Space X (sInf T)

Full source

protected theorem R1Space.sInf {X : Type*} {T : Set (TopologicalSpace X)}
    (hT : ∀ t ∈ T, @R1Space X t) : @R1Space X (sInf T) := by
  let _ := sInf T
  refine ⟨fun x y ↦ ?_⟩
  simp only [Specializes, nhds_sInf]
  rcases em (∃ t ∈ T, Disjoint (@nhds X t x) (@nhds X t y)) with ⟨t, htT, htd⟩ | hTd
  · exact .inr <| htd.mono (iInf₂_le t htT) (iInf₂_le t htT)
  · push_neg at hTd
    exact .inl <| iInf₂_mono fun t ht ↦ ((hT t ht).1 x y).resolve_right (hTd t ht)

Infimum of R₁ Spaces is R₁

Informal description

Let $ X $ be a type and $ T $ be a set of topological spaces on $ X $. If every topological space $ t \in T $ is an R₁ space, then the infimum of $ T $ (i.e., the coarsest topology on $ X $ that is finer than every $ t \in T $) is also an R₁ space.

R1Space.iInf theorem

{ι X : Type*} {t : ι → TopologicalSpace X} (ht : ∀ i, @R1Space X (t i)) : @R1Space X (iInf t)

Full source

protected theorem R1Space.iInf {ι X : Type*} {t : ι → TopologicalSpace X}
    (ht : ∀ i, @R1Space X (t i)) : @R1Space X (iInf t) :=
  .sInf <| forall_mem_range.2 ht

Infimum of R₁ Spaces is R₁

Informal description

Let $X$ be a type and $\{t_i\}_{i \in \iota}$ be a family of topological spaces on $X$. If for every index $i \in \iota$, the topological space $t_i$ is an R₁ space, then the infimum topology $\bigsqcap_{i \in \iota} t_i$ (i.e., the coarsest topology on $X$ that is finer than every $t_i$) is also an R₁ space.

R1Space.inf theorem

 {X : Type*} {t₁ t₂ : TopologicalSpace X} (h₁ : @R1Space X t₁) (h₂ : @R1Space X t₂) : @R1Space X (t₁ ⊓ t₂)

Full source

protected theorem R1Space.inf {X : Type*} {t₁ t₂ : TopologicalSpace X}
    (h₁ : @R1Space X t₁) (h₂ : @R1Space X t₂) : @R1Space X (t₁ ⊓ t₂) := by
  rw [inf_eq_iInf]
  apply R1Space.iInf
  simp [*]

Infimum of Two R₁ Topologies is R₁

Informal description

Let $X$ be a topological space with two topologies $t_1$ and $t_2$. If both $t_1$ and $t_2$ are R₁ (preregular) spaces, then the infimum topology $t_1 \sqcap t_2$ (the coarsest topology finer than both $t_1$ and $t_2$) is also an R₁ space.

instR1SpaceProd instance

[TopologicalSpace Y] [R1Space Y] : R1Space (X × Y)

Full source

instance [TopologicalSpace Y] [R1Space Y] : R1Space (X × Y) :=
  .inf (.induced _) (.induced _)

Product of an R₁ Space is R₁

Informal description

For any two topological spaces $X$ and $Y$ where $Y$ is an R₁ (preregular) space, the product space $X \times Y$ is also an R₁ space.

instR1SpaceForall instance

{ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, R1Space (X i)] : R1Space (∀ i, X i)

Full source

instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, R1Space (X i)] :
    R1Space (∀ i, X i) :=
  .iInf fun _ ↦ .induced _

Product of R₁ Spaces is R₁

Informal description

For any family of topological spaces $\{X_i\}_{i \in \iota}$ where each $X_i$ is an R₁ (preregular) space, the product space $\prod_{i \in \iota} X_i$ equipped with the product topology is also an R₁ space.

exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds theorem

 {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [R1Space Y] {f : X → Y} {x : X} {K : Set X} {s : Set Y}
  (hf : Continuous f) (hs : s ∈ 𝓝 (f x)) (hKc : IsCompact K) (hKx : K ∈ 𝓝 x) : ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s

Full source

theorem exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds
    {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [R1Space Y] {f : X → Y} {x : X}
    {K : Set X} {s : Set Y} (hf : Continuous f) (hs : s ∈ 𝓝 (f x)) (hKc : IsCompact K)
    (hKx : K ∈ 𝓝 x) : ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s := by
  have hc : IsCompact (f '' Kf '' K \ interior s) := (hKc.image hf).diff isOpen_interior
  obtain ⟨U, V, Uo, Vo, hxU, hV, hd⟩ : SeparatedNhds {f x} (f '' Kf '' K \ interior s) := by
    simp_rw [separatedNhds_iff_disjoint, nhdsSet_singleton, hc.disjoint_nhdsSet_right,
      disjoint_nhds_nhds_iff_not_inseparable]
    rintro y ⟨-, hys⟩ hxy
    refine hys <| (hxy.mem_open_iff isOpen_interior).1 ?_
    rwa [mem_interior_iff_mem_nhds]
  refine ⟨K \ f ⁻¹' V, diff_mem hKx ?_, hKc.diff <| Vo.preimage hf, fun y hy ↦ ?_⟩
  · filter_upwards [hf.continuousAt <| Uo.mem_nhds (hxU rfl)] with x hx
      using Set.disjoint_left.1 hd hx
  · by_contra hys
    exact hy.2 (hV ⟨mem_image_of_mem _ hy.1, not_mem_subset interior_subset hys⟩)

Existence of Compact Neighborhood Mapping to Given Neighborhood in R₁ Space

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ an R₁ (preregular) space. Given a continuous function $f : X \to Y$, a point $x \in X$, a compact set $K \subseteq X$ containing $x$ in its neighborhood, and a neighborhood $s$ of $f(x)$ in $Y$, there exists a neighborhood $L$ of $x$ in $X$ such that $L$ is compact and $f(L) \subseteq s$.

instLocallyCompactPairOfWeaklyLocallyCompactSpaceOfR1Space instance

 {X Y : Type*} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [TopologicalSpace Y] [R1Space Y] :
  LocallyCompactPair X Y

Full source

instance (priority := 900) {X Y : Type*} [TopologicalSpace X] [WeaklyLocallyCompactSpace X]
    [TopologicalSpace Y] [R1Space Y] : LocallyCompactPair X Y where
  exists_mem_nhds_isCompact_mapsTo hf hs :=
    let ⟨_K, hKc, hKx⟩ := exists_compact_mem_nhds _
    exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds hf hs hKc hKx

Weakly Locally Compact and R₁ Spaces Form Locally Compact Pairs

Informal description

For any topological spaces $X$ and $Y$, if $X$ is weakly locally compact and $Y$ is an R₁ (preregular) space, then $(X, Y)$ forms a locally compact pair. This means that for any continuous function $f : X \to Y$, point $x \in X$, and compact neighborhood $K$ of $x$ in $X$, there exists a compact neighborhood $L$ of $x$ contained in $K$ such that $f(L)$ is contained in some neighborhood of $f(x)$ in $Y$.

IsCompact.isCompact_isClosed_basis_nhds theorem

 {x : X} {L : Set X} (hLc : IsCompact L) (hxL : L ∈ 𝓝 x) :
  (𝓝 x).HasBasis (fun K ↦ K ∈ 𝓝 x ∧ IsCompact K ∧ IsClosed K) (·)

Full source

/-- If a point in an R₁ space has a compact neighborhood,
then it has a basis of compact closed neighborhoods. -/
theorem IsCompact.isCompact_isClosed_basis_nhds {x : X} {L : Set X} (hLc : IsCompact L)
    (hxL : L ∈ 𝓝 x) : (𝓝 x).HasBasis (fun K ↦ K ∈ 𝓝 xK ∈ 𝓝 x ∧ IsCompact K ∧ IsClosed K) (·) :=
  hasBasis_self.2 fun _U hU ↦
    let ⟨K, hKx, hKc, hKU⟩ := exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds
      continuous_id (interior_mem_nhds.2 hU) hLc hxL
    ⟨closure K, mem_of_superset hKx subset_closure, ⟨hKc.closure, isClosed_closure⟩,
      (hKc.closure_subset_of_isOpen isOpen_interior hKU).trans interior_subset⟩

Existence of Compact Closed Neighborhood Basis in R₁ Spaces

Informal description

Let $ X $ be an R₁ space, $ x \in X $ a point, and $ L \subseteq X $ a compact neighborhood of $ x $. Then the neighborhood filter of $ x $ has a basis consisting of compact closed neighborhoods. That is, for any neighborhood $ U $ of $ x $, there exists a neighborhood $ K $ of $ x $ such that $ K \subseteq U $, $ K $ is compact, and $ K $ is closed.

Filter.coclosedCompact_eq_cocompact theorem

: coclosedCompact X = cocompact X

Full source

/-- In an R₁ space, the filters `coclosedCompact` and `cocompact` are equal. -/
@[simp]
theorem Filter.coclosedCompact_eq_cocompact : coclosedCompact X = cocompact X := by
  refine le_antisymm ?_ cocompact_le_coclosedCompact
  rw [hasBasis_coclosedCompact.le_basis_iff hasBasis_cocompact]
  exact fun K hK ↦ ⟨closure K, ⟨isClosed_closure, hK.closure⟩, compl_subset_compl.2 subset_closure⟩

Equality of Coclosed-Compact and Cocompact Filters in R₁ Spaces

Informal description

In a preregular (R₁) topological space $X$, the coclosed-compact filter is equal to the cocompact filter. That is, a subset of $X$ has a closed and compact complement if and only if it has a compact complement.

Bornology.relativelyCompact_eq_inCompact theorem

: Bornology.relativelyCompact X = Bornology.inCompact X

Full source

/-- In an R₁ space, the bornologies `relativelyCompact` and `inCompact` are equal. -/
@[simp]
theorem Bornology.relativelyCompact_eq_inCompact :
    Bornology.relativelyCompact X = Bornology.inCompact X :=
  Bornology.ext _ _ Filter.coclosedCompact_eq_cocompact

Equality of Relatively Compact and In-Compact Bornologies in R₁ Spaces

Informal description

In a preregular (R₁) topological space $X$, the bornology of relatively compact sets (sets with compact closure) coincides with the bornology of sets contained in a compact set.

isCompact_isClosed_basis_nhds theorem

(x : X) : (𝓝 x).HasBasis (fun K => K ∈ 𝓝 x ∧ IsCompact K ∧ IsClosed K) (·)

Full source

/-- In a (weakly) locally compact R₁ space, compact closed neighborhoods of a point `x`
form a basis of neighborhoods of `x`. -/
theorem isCompact_isClosed_basis_nhds (x : X) :
    (𝓝 x).HasBasis (fun K => K ∈ 𝓝 xK ∈ 𝓝 x ∧ IsCompact K ∧ IsClosed K) (·) :=
  let ⟨_L, hLc, hLx⟩ := exists_compact_mem_nhds x
  hLc.isCompact_isClosed_basis_nhds hLx

Existence of Compact Closed Neighborhood Basis in Weakly Locally Compact R₁ Spaces

Informal description

In a weakly locally compact preregular (R₁) space $X$, for every point $x \in X$, the neighborhood filter of $x$ has a basis consisting of compact closed neighborhoods. That is, for any neighborhood $U$ of $x$, there exists a neighborhood $K$ of $x$ such that $K \subseteq U$, $K$ is compact, and $K$ is closed.

exists_mem_nhds_isCompact_isClosed theorem

(x : X) : ∃ K ∈ 𝓝 x, IsCompact K ∧ IsClosed K

Full source

/-- In a (weakly) locally compact R₁ space, each point admits a compact closed neighborhood. -/
theorem exists_mem_nhds_isCompact_isClosed (x : X) : ∃ K ∈ 𝓝 x, IsCompact K ∧ IsClosed K :=
  (isCompact_isClosed_basis_nhds x).ex_mem

Existence of Compact Closed Neighborhoods in Weakly Locally Compact R₁ Spaces

Informal description

For every point $x$ in a weakly locally compact preregular (R₁) space $X$, there exists a neighborhood $K$ of $x$ that is both compact and closed.

WeaklyLocallyCompactSpace.locallyCompactSpace instance

: LocallyCompactSpace X

Full source

/-- A weakly locally compact R₁ space is locally compact. -/
instance (priority := 80) WeaklyLocallyCompactSpace.locallyCompactSpace : LocallyCompactSpace X :=
  .of_hasBasis isCompact_isClosed_basis_nhds fun _ _ ⟨_, h, _⟩ ↦ h

Weakly Locally Compact R₁ Spaces are Locally Compact

Informal description

Every weakly locally compact preregular (R₁) space is locally compact.

exists_isOpen_superset_and_isCompact_closure theorem

{K : Set X} (hK : IsCompact K) : ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)

Full source

/-- In a weakly locally compact R₁ space,
every compact set has an open neighborhood with compact closure. -/
theorem exists_isOpen_superset_and_isCompact_closure {K : Set X} (hK : IsCompact K) :
    ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V) := by
  rcases exists_compact_superset hK with ⟨K', hK', hKK'⟩
  exact ⟨interior K', isOpen_interior, hKK', hK'.closure_of_subset interior_subset⟩

Existence of Open Neighborhood with Compact Closure for Compact Sets in Weakly Locally Compact R₁ Spaces

Informal description

Let $X$ be a weakly locally compact R₁ space and $K \subseteq X$ a compact set. Then there exists an open set $V \subseteq X$ such that $K \subseteq V$ and the closure $\overline{V}$ is compact.

exists_isOpen_mem_isCompact_closure theorem

(x : X) : ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)

Full source

/-- In a weakly locally compact R₁ space,
every point has an open neighborhood with compact closure. -/
theorem exists_isOpen_mem_isCompact_closure (x : X) :
    ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U) := by
  simpa only [singleton_subset_iff]
    using exists_isOpen_superset_and_isCompact_closure isCompact_singleton

Existence of Compact-Closure Neighborhoods in Weakly Locally Compact R₁ Spaces

Informal description

Let $X$ be a weakly locally compact R₁ space. For every point $x \in X$, there exists an open neighborhood $U$ of $x$ such that the closure $\overline{U}$ is compact.

Mathlib.Topology.Separation.Basic

Main definitions

Main results

T₀ spaces

T₁ spaces

References