Separation properties of topological spaces

This file defines some of the weaker separation axioms (under the Kolmogorov classification), notably T₀, R₀, T₁ and R₁ spaces. For T₂ (Hausdorff) spaces and other stronger conditions, see the file Topology/Separation/Hausdorff.lean.

Main definitions

• SeparatedNhds: Two Sets are separated by neighbourhoods if they are contained in disjoint open sets.
• HasSeparatingCover: A set has a countable cover that can be used with hasSeparatingCovers_iff_separatedNhds to witness when two Sets have SeparatedNhds.
• T0Space: A T₀/Kolmogorov space is a space where, for every two points x ≠ y, there is an open set that contains one, but not the other.
• R0Space: An R₀ space (sometimes called a symmetric space) is a topological space such that the Specializes relation is symmetric.
• T1Space: A T₁/Fréchet space is a space where every singleton set is closed. This is equivalent to, for every pair x ≠ y, there existing an open set containing x but not y (t1Space_iff_exists_open shows that these conditions are equivalent.) T₁ implies T₀ and R₀.
• R1Space: An R₁/preregular space is a space where any two topologically distinguishable points have disjoint neighbourhoods. R₁ implies R₀.

Note that mathlib adopts the modern convention that m ≤ n if and only if T_m → T_n, but occasionally the literature swaps definitions for e.g. T₃ and regular.

Main results

T₀ spaces

• IsClosed.exists_closed_singleton: Given a closed set S in a compact T₀ space, there is some x ∈ S such that {x} is closed.
• exists_isOpen_singleton_of_isOpen_finite: Given an open finite set S in a T₀ space, there is some x ∈ S such that {x} is open.

T₁ spaces

• isClosedMap_const: The constant map is a closed map.
• Finite.instDiscreteTopology: A finite T₁ space must have the discrete topology.

References

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

class T0Space (X : Type u) [TopologicalSpace X] : Prop

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.

• t0 ⦃x y : X⦄ : Inseparable x y → x = y

  Two inseparable points in a T₀ space are equal.

Instances

• ContinuousMap.instT0Space
• ContinuousMapZero.instT0Space
• EMetricSpace.instT0Space
• Filter.instT0Space
• MetricSpace.instT0Space
• Pi.instT0Space
• Prod.instT0Space
• SeparationQuotient.instT0Space
• Subtype.t0Space
• T1Space.t0Space
• TopologicalSpace.Opens.CompleteCopy.instT0Space
• ULift.instT0Space
• UniformSpace.Completion.t0Space

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

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

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

theorem Topology.IsInducing.injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] {f : X → Y} (hf : IsInducing f) : Function.Injective f

A topology inducing map from a T₀ space is injective.

@[deprecated Topology.IsInducing.injective (since := "2024-10-28")]

theorem Inducing.injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] {f : X → Y} (hf : Topology.IsInducing f) : Function.Injective f

Alias of Topology.IsInducing.injective.

---

A topology inducing map from a T₀ space is injective.

theorem Topology.IsInducing.isEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] {f : X → Y} (hf : IsInducing f) : IsEmbedding f

A topology inducing map from a T₀ space is a topological embedding.

@[deprecated Topology.IsInducing.isEmbedding (since := "2024-10-28")]

theorem Inducing.isEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] {f : X → Y} (hf : Topology.IsInducing f) : Topology.IsEmbedding f

Alias of Topology.IsInducing.isEmbedding.

---

A topology inducing map from a T₀ space is a topological embedding.

@[deprecated Topology.IsInducing.isEmbedding (since := "2024-10-26")]

theorem Inducing.embedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] {f : X → Y} (hf : Topology.IsInducing f) : Topology.IsEmbedding f

Alias of Topology.IsInducing.isEmbedding.

---

A topology inducing map from a T₀ space is a topological embedding.

theorem isEmbedding_iff_isInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] {f : X → Y} : Topology.IsEmbedding f ↔ Topology.IsInducing f

@[deprecated isEmbedding_iff_isInducing (since := "2024-10-28")]

theorem isEmbedding_iff_inducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] {f : X → Y} : Topology.IsEmbedding f ↔ Topology.IsInducing f

Alias of isEmbedding_iff_isInducing.

@[deprecated isEmbedding_iff_isInducing (since := "2024-10-26")]

theorem embedding_iff_inducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] {f : X → Y} : Topology.IsEmbedding f ↔ Topology.IsInducing f

Alias of isEmbedding_iff_isInducing.

theorem t0Space_iff_nhds_injective (X : Type u) [TopologicalSpace X] : T0Space X ↔ Function.Injective nhds

theorem nhds_injective {X : Type u_1} [TopologicalSpace X] [T0Space X] : Function.Injective nhds

theorem inseparable_iff_eq {X : Type u_1} [TopologicalSpace X] [T0Space X] {x y : X} : Inseparable x y ↔ x = y

@[simp]

theorem nhds_eq_nhds_iff {X : Type u_1} [TopologicalSpace X] [T0Space X] {a b : X} : nhds a = nhds b ↔ a = b

@[simp]

theorem inseparable_eq_eq {X : Type u_1} [TopologicalSpace X] [T0Space X] : Inseparable = Eq

theorem TopologicalSpace.IsTopologicalBasis.inseparable_iff {X : Type u_1} [TopologicalSpace X] {b : Set (Set X)} (hb : IsTopologicalBasis b) {x y : X} : Inseparable x y ↔ ∀ s ∈ b, x ∈ s ↔ y ∈ s

theorem TopologicalSpace.IsTopologicalBasis.eq_iff {X : Type u_1} [TopologicalSpace X] [T0Space X] {b : Set (Set X)} (hb : IsTopologicalBasis b) {x y : X} : x = y ↔ ∀ s ∈ b, x ∈ s ↔ y ∈ s

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

theorem exists_isOpen_xor'_mem {X : Type u_1} [TopologicalSpace X] [T0Space X] {x y : X} (h : x ≠ y) : ∃ (U : Set X), IsOpen U ∧ Xor' (x ∈ U) (y ∈ U)

def specializationOrder (X : Type u_3) [TopologicalSpace X] [T0Space X] : PartialOrder X

Specialization forms a partial order on a t0 topological space.

Equations

• specializationOrder X = PartialOrder.mk ⋯

instance SeparationQuotient.instT0Space {X : Type u_1} [TopologicalSpace X] : T0Space (SeparationQuotient X)

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

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

theorem IsClosed.exists_closed_singleton {X : Type u_1} [TopologicalSpace X] [T0Space X] [CompactSpace X] {S : Set X} (hS : IsClosed S) (hne : S.Nonempty) : ∃ x ∈ S, IsClosed {x}

Given a closed set S in a compact T₀ space, there is some x ∈ S such that {x} is closed.

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

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

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

Given an open finite set S in a T₀ space, there is some x ∈ S such that {x} is open.

theorem exists_open_singleton_of_finite {X : Type u_1} [TopologicalSpace X] [T0Space X] [Finite X] [Nonempty X] : ∃ (x : X), IsOpen {x}

theorem t0Space_of_injective_of_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Function.Injective f) (hf' : Continuous f) [T0Space Y] : T0Space X

theorem Topology.IsEmbedding.t0Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space Y] {f : X → Y} (hf : IsEmbedding f) : T0Space X

@[deprecated Topology.IsEmbedding.t0Space (since := "2024-10-26")]

theorem Embedding.t0Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space Y] {f : X → Y} (hf : Topology.IsEmbedding f) : T0Space X

Alias of Topology.IsEmbedding.t0Space.

instance Subtype.t0Space {X : Type u_1} [TopologicalSpace X] [T0Space X] {p : X → Prop} : T0Space (Subtype p)

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

instance Prod.instT0Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] [T0Space Y] : T0Space (X × Y)

instance Pi.instT0Space {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T0Space (X i)] : T0Space ((i : ι) → X i)

instance ULift.instT0Space {X : Type u_1} [TopologicalSpace X] [T0Space X] : T0Space (ULift.{u_3, u_1} X)

theorem T0Space.of_cover {X : Type u_1} [TopologicalSpace X] (h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space ↑s) : T0Space X

theorem T0Space.of_open_cover {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), ∃ (s : Set X), x ∈ s ∧ IsOpen s ∧ T0Space ↑s) : T0Space X

class R0Space (X : Type u) [TopologicalSpace X] : Prop

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.

• specializes_symmetric : Symmetric Specializes

  In an R₀ space, the Specializes relation is symmetric.

Instances

• ContinuousMap.instR0Space
• ContinuousMapZero.instR0Space
• instR0Space
• instR0SpaceForall
• instR0SpaceOfT1Space
• instR0SpaceProd
• instR0SpaceSubtype

theorem r0Space_iff (X : Type u) [TopologicalSpace X] : R0Space X ↔ Symmetric Specializes

theorem Specializes.symm {X : Type u_1} [TopologicalSpace X] [R0Space X] {x y : X} (h : x ⤳ y) : y ⤳ x

In an R₀ space, the Specializes relation is symmetric, dot notation version.

theorem specializes_comm {X : Type u_1} [TopologicalSpace X] [R0Space X] {x y : X} : x ⤳ y ↔ y ⤳ x

In an R₀ space, the Specializes relation is symmetric, Iff version.

theorem specializes_iff_inseparable {X : Type u_1} [TopologicalSpace X] [R0Space X] {x y : X} : x ⤳ y ↔ Inseparable x y

In an R₀ space, Specializes is equivalent to Inseparable.

theorem Specializes.inseparable {X : Type u_1} [TopologicalSpace X] [R0Space X] {x y : X} : x ⤳ y → Inseparable x y

In an R₀ space, Specializes implies Inseparable.

theorem Topology.IsInducing.r0Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R0Space X] [TopologicalSpace Y] {f : Y → X} (hf : IsInducing f) : R0Space Y

@[deprecated Topology.IsInducing.r0Space (since := "2024-10-28")]

theorem Inducing.r0Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R0Space X] [TopologicalSpace Y] {f : Y → X} (hf : Topology.IsInducing f) : R0Space Y

Alias of Topology.IsInducing.r0Space.

instance instR0SpaceSubtype {X : Type u_1} [TopologicalSpace X] [R0Space X] {p : X → Prop} : R0Space { x : X // p x }

instance instR0SpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R0Space X] [TopologicalSpace Y] [R0Space Y] : R0Space (X × Y)

instance instR0SpaceForall {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), R0Space (X i)] : R0Space ((i : ι) → X i)

theorem isCompact_closure_singleton {X : Type u_1} [TopologicalSpace X] [R0Space X] {x : X} : IsCompact (closure {x})

In an R₀ space, the closure of a singleton is a compact set.

theorem Filter.coclosedCompact_le_cofinite {X : Type u_1} [TopologicalSpace X] [R0Space X] : coclosedCompact X ≤ cofinite

def Bornology.relativelyCompact (X : Type u_1) [TopologicalSpace X] [R0Space X] : Bornology X

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.

Equations

• Bornology.relativelyCompact X = { cobounded' := Filter.coclosedCompact X, le_cofinite' := ⋯ }

theorem Bornology.relativelyCompact.isBounded_iff {X : Type u_1} [TopologicalSpace X] [R0Space X] {s : Set X} : IsBounded s ↔ IsCompact (closure s)

theorem Set.Finite.isCompact_closure {X : Type u_1} [TopologicalSpace X] [R0Space X] {s : Set X} (hs : s.Finite) : IsCompact (closure s)

In an R₀ space, the closure of a finite set is a compact set.

class T1Space (X : Type u) [TopologicalSpace X] : Prop

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.

• t1 (x : X) : IsClosed {x}

  A singleton in a T₁ space is a closed set.

Instances

• ContinuousMap.instT1Space
• ContinuousMapZero.instT1Space
• MeasureTheory.t1Space_probabilityMeasure_of_finite
• Subtype.t1Space
• T2Space.t1Space
• TotallyDisconnectedSpace.t1Space
• ULift.instT1Space
• instT1SpaceCofiniteTopology
• instT1SpaceForall
• instT1SpaceProd

theorem isClosed_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} : IsClosed {x}

theorem isOpen_compl_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} : IsOpen {x}ᶜ

theorem isOpen_ne {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} : IsOpen {y : X | y ≠ x}

theorem Continuous.isOpen_mulSupport {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] [One X] [TopologicalSpace Y] {f : Y → X} (hf : Continuous f) : IsOpen (Function.mulSupport f)

theorem Continuous.isOpen_support {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] [Zero X] [TopologicalSpace Y] {f : Y → X} (hf : Continuous f) : IsOpen (Function.support f)

theorem Ne.nhdsWithin_compl_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} (h : x ≠ y) : nhdsWithin x {y}ᶜ = nhds x

theorem Ne.nhdsWithin_diff_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} (h : x ≠ y) (s : Set X) : nhdsWithin x (s \ {y}) = nhdsWithin x s

theorem nhdsWithin_compl_singleton_le {X : Type u_1} [TopologicalSpace X] [T1Space X] (x y : X) : nhdsWithin x {x}ᶜ ≤ nhdsWithin x {y}ᶜ

theorem isOpen_setOf_eventually_nhdsWithin {X : Type u_1} [TopologicalSpace X] [T1Space X] {p : X → Prop} : IsOpen {x : X | ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, p y}

theorem Set.Finite.isClosed {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} (hs : s.Finite) : IsClosed s

theorem TopologicalSpace.IsTopologicalBasis.exists_mem_of_ne {X : Type u_1} [TopologicalSpace X] [T1Space X] {b : Set (Set X)} (hb : IsTopologicalBasis b) {x y : X} (h : x ≠ y) : ∃ a ∈ b, x ∈ a ∧ y ∉ a

theorem Finset.isClosed {X : Type u_1} [TopologicalSpace X] [T1Space X] (s : Finset X) : IsClosed ↑s

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

theorem t1Space_iff_continuous_cofinite_of {X : Type u_1} [TopologicalSpace X] : T1Space X ↔ Continuous ⇑CofiniteTopology.of

theorem CofiniteTopology.continuous_of {X : Type u_1} [TopologicalSpace X] [T1Space X] : Continuous ⇑of

theorem t1Space_iff_exists_open {X : Type u_1} [TopologicalSpace X] : T1Space X ↔ Pairwise fun (x y : X) => ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ y ∉ U

theorem t1Space_iff_disjoint_pure_nhds {X : Type u_1} [TopologicalSpace X] : T1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (nhds y)

theorem t1Space_iff_disjoint_nhds_pure {X : Type u_1} [TopologicalSpace X] : T1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (nhds x) (pure y)

theorem t1Space_iff_specializes_imp_eq {X : Type u_1} [TopologicalSpace X] : T1Space X ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y

theorem disjoint_pure_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} (h : x ≠ y) : Disjoint (pure x) (nhds y)

theorem disjoint_nhds_pure {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} (h : x ≠ y) : Disjoint (nhds x) (pure y)

theorem Specializes.eq {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} (h : x ⤳ y) : x = y

theorem specializes_iff_eq {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} : x ⤳ y ↔ x = y

@[simp]

theorem specializes_eq_eq {X : Type u_1} [TopologicalSpace X] [T1Space X] : (fun (x1 x2 : X) => x1 ⤳ x2) = Eq

@[simp]

theorem pure_le_nhds_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {a b : X} : pure a ≤ nhds b ↔ a = b

@[simp]

theorem nhds_le_nhds_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {a b : X} : nhds a ≤ nhds b ↔ a = b

@[instance 100]

instance instR0SpaceOfT1Space {X : Type u_1} [TopologicalSpace X] [T1Space X] : R0Space X

instance instT1SpaceCofiniteTopology {X : Type u_1} : T1Space (CofiniteTopology X)

theorem t1Space_antitone {X : Type u_3} : Antitone (@T1Space X)

theorem continuousWithinAt_update_of_ne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [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'

theorem continuousAt_update_of_ne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [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'

theorem continuousOn_update_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [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 → Filter.Tendsto f (nhdsWithin x (s \ {x})) (nhds y))

theorem t1Space_of_injective_of_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Function.Injective f) (hf' : Continuous f) [T1Space Y] : T1Space X

theorem Topology.IsEmbedding.t1Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {f : X → Y} (hf : IsEmbedding f) : T1Space X

@[deprecated Topology.IsEmbedding.t1Space (since := "2024-10-26")]

theorem Embedding.t1Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {f : X → Y} (hf : Topology.IsEmbedding f) : T1Space X

Alias of Topology.IsEmbedding.t1Space.

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

instance instT1SpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space X] [T1Space Y] : T1Space (X × Y)

instance instT1SpaceForall {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T1Space (X i)] : T1Space ((i : ι) → X i)

instance ULift.instT1Space {X : Type u_1} [TopologicalSpace X] [T1Space X] : T1Space (ULift.{u_3, u_1} X)

@[instance 100]

instance TotallyDisconnectedSpace.t1Space {X : Type u_1} [TopologicalSpace X] [h : TotallyDisconnectedSpace X] : T1Space X

@[instance 100]

instance T1Space.t0Space {X : Type u_1} [TopologicalSpace X] [T1Space X] : T0Space X

@[simp]

theorem compl_singleton_mem_nhds_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} : {x}ᶜ ∈ nhds y ↔ y ≠ x

theorem compl_singleton_mem_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} (h : y ≠ x) : {x}ᶜ ∈ nhds y

@[simp]

theorem closure_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} : closure {x} = {x}

theorem Set.Subsingleton.closure {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} (hs : s.Subsingleton) : (_root_.closure s).Subsingleton

@[simp]

theorem subsingleton_closure {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} : (closure s).Subsingleton ↔ s.Subsingleton

theorem isClosedMap_const {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {y : Y} : IsClosedMap (Function.const X y)

theorem isClosedMap_prodMk_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space X] (x : X) : IsClosedMap fun (y : Y) => (x, y)

theorem isClosedMap_prodMk_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] (y : Y) : IsClosedMap fun (x : X) => (x, y)

theorem nhdsWithin_insert_of_ne {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} {s : Set X} (hxy : x ≠ y) : nhdsWithin x (insert y s) = nhdsWithin x s

theorem insert_mem_nhdsWithin_of_subset_insert {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} {s t : Set X} (hu : t ⊆ insert y s) : insert x s ∈ nhdsWithin x t

If t is a subset of s, except for one point, then insert x s is a neighborhood of x within t.

theorem eventuallyEq_insert {X : Type u_1} [TopologicalSpace X] [T1Space X] {s t : Set X} {x y : X} (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) : insert x s =ᶠ[nhds x] insert x t

@[simp]

theorem ker_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] (x : X) : (nhds x).ker = {x}

theorem biInter_basis_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {x : X} (h : (nhds x).HasBasis p s) : ⋂ (i : ι), ⋂ (_ : p i), s i = {x}

@[simp]

theorem compl_singleton_mem_nhdsSet_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {s : Set X} : {x}ᶜ ∈ nhdsSet s ↔ x ∉ s

@[simp]

theorem nhdsSet_le_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {s t : Set X} : nhdsSet s ≤ nhdsSet t ↔ s ⊆ t

@[simp]

theorem nhdsSet_inj_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {s t : Set X} : nhdsSet s = nhdsSet t ↔ s = t

theorem injective_nhdsSet {X : Type u_1} [TopologicalSpace X] [T1Space X] : Function.Injective nhdsSet

theorem strictMono_nhdsSet {X : Type u_1} [TopologicalSpace X] [T1Space X] : StrictMono nhdsSet

@[simp]

theorem nhds_le_nhdsSet_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} {x : X} : nhds x ≤ nhdsSet s ↔ x ∈ s

theorem Dense.diff_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} (hs : Dense s) (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : Dense (s \ {x})

Removing a non-isolated point from a dense set, one still obtains a dense set.

theorem Dense.diff_finset {X : Type u_1} [TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X} (hs : Dense s) (t : Finset X) : Dense (s \ ↑t)

Removing a finset from a dense set in a space without isolated points, one still obtains a dense set.

theorem Dense.diff_finite {X : Type u_1} [TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X} (hs : Dense s) {t : Set X} (ht : t.Finite) : Dense (s \ t)

Removing a finite set from a dense set in a space without isolated points, one still obtains a dense set.

theorem eq_of_tendsto_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {f : X → Y} {x : X} {y : Y} (h : Filter.Tendsto f (nhds x) (nhds y)) : f x = y

If a function to a T1Space tends to some limit y at some point x, then necessarily y = f x.

theorem Filter.Tendsto.eventually_ne {Y : Type u_2} {X : Type u_3} [TopologicalSpace Y] [T1Space Y] {g : X → Y} {l : Filter X} {b₁ b₂ : Y} (hg : Tendsto g l (nhds b₁)) (hb : b₁ ≠ b₂) : ∀ᶠ (z : X) in l, g z ≠ b₂

theorem ContinuousAt.eventually_ne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {g : X → Y} {x : X} {y : Y} (hg1 : ContinuousAt g x) (hg2 : g x ≠ y) : ∀ᶠ (z : X) in nhds x, g z ≠ y

theorem eventually_ne_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] {a b : X} (h : a ≠ b) : ∀ᶠ (x : X) in nhds a, x ≠ b

theorem eventually_ne_nhdsWithin {X : Type u_1} [TopologicalSpace X] [T1Space X] {a b : X} {s : Set X} (h : a ≠ b) : ∀ᶠ (x : X) in nhdsWithin a s, x ≠ b

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

theorem ContinuousWithinAt.of_insert {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space X] {x y : X} {s : Set X} {f : X → Y} : ContinuousWithinAt f (insert y s) x → ContinuousWithinAt f s x

Alias of the forward direction of continuousWithinAt_insert.

theorem ContinuousWithinAt.insert' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space X] {x y : X} {s : Set X} {f : X → Y} : ContinuousWithinAt f s x → ContinuousWithinAt f (insert y s) x

Alias of the reverse direction of continuousWithinAt_insert.

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

See also continuousWithinAt_diff_self for the case y = x but not requiring T1Space.

theorem continuousWithinAt_congr_set' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space X] {x : X} {s t : Set X} {f : X → Y} (y : X) (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) : ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

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 continuousAt_of_tendsto_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {f : X → Y} {x : X} {y : Y} (h : Filter.Tendsto f (nhds x) (nhds y)) : ContinuousAt f x

To prove a function to a T1Space is continuous at some point x, it suffices to prove that f admits some limit at x.

@[simp]

theorem tendsto_const_nhds_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] {l : Filter Y} [l.NeBot] {c d : X} : Filter.Tendsto (fun (x : Y) => c) l (nhds d) ↔ c = d

theorem isOpen_singleton_of_finite_mem_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] (x : X) {s : Set X} (hs : s ∈ nhds x) (hsf : s.Finite) : IsOpen {x}

A point with a finite neighborhood has to be isolated.

theorem infinite_of_mem_nhds {X : Type u_3} [TopologicalSpace X] [T1Space X] (x : X) [hx : (nhdsWithin x {x}ᶜ).NeBot] {s : Set X} (hs : s ∈ nhds x) : s.Infinite

If the punctured neighborhoods of a point form a nontrivial filter, then any neighborhood is infinite.

instance Finite.instDiscreteTopology {X : Type u_1} [TopologicalSpace X] [T1Space X] [Finite X] : DiscreteTopology X

theorem Set.Finite.continuousOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] [TopologicalSpace Y] {s : Set X} (hs : s.Finite) (f : X → Y) : ContinuousOn f s

theorem PreconnectedSpace.trivial_of_discrete {X : Type u_1} [TopologicalSpace X] [PreconnectedSpace X] [DiscreteTopology X] : Subsingleton X

theorem IsPreconnected.infinite_of_nontrivial {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} (h : IsPreconnected s) (hs : s.Nontrivial) : s.Infinite

theorem ConnectedSpace.infinite {X : Type u_1} [TopologicalSpace X] [ConnectedSpace X] [Nontrivial X] [T1Space X] : Infinite X

@[instance 100]

instance ConnectedSpace.neBot_nhdsWithin_compl_of_nontrivial_of_t1space {X : Type u_1} [TopologicalSpace X] [ConnectedSpace X] [Nontrivial X] [T1Space X] (x : X) : (nhdsWithin x {x}ᶜ).NeBot

A non-trivial connected T1 space has no isolated points.

theorem SeparationQuotient.t1Space_iff {X : Type u_1} [TopologicalSpace X] : T1Space (SeparationQuotient X) ↔ R0Space X

theorem Set.Subsingleton.isClosed {X : Type u_1} [TopologicalSpace X] [T1Space X] {A : Set X} (h : A.Subsingleton) : IsClosed A

theorem isClosed_inter_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {A : Set X} {a : X} : IsClosed (A ∩ {a})

theorem isClosed_singleton_inter {X : Type u_1} [TopologicalSpace X] [T1Space X] {A : Set X} {a : X} : IsClosed ({a} ∩ A)

theorem singleton_mem_nhdsWithin_of_mem_discrete {X : Type u_1} [TopologicalSpace X] {s : Set X} [DiscreteTopology ↑s] {x : X} (hx : x ∈ s) : {x} ∈ nhdsWithin x s

theorem nhdsWithin_of_mem_discrete {X : Type u_1} [TopologicalSpace X] {s : Set X} [DiscreteTopology ↑s] {x : X} (hx : x ∈ s) : nhdsWithin x s = pure x

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 Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {p : ι → Prop} {t : ι → Set X} {s : Set X} [DiscreteTopology ↑s] {x : X} (hb : (nhds x).HasBasis p t) (hx : x ∈ s) : ∃ (i : ι), p i ∧ t i ∩ s = {x}

theorem nhds_inter_eq_singleton_of_mem_discrete {X : Type u_1} [TopologicalSpace X] {s : Set X} [DiscreteTopology ↑s] {x : X} (hx : x ∈ s) : ∃ U ∈ nhds x, U ∩ s = {x}

A point x in a discrete subset s of a topological space admits a neighbourhood that only meets s at x.

theorem isOpen_inter_eq_singleton_of_mem_discrete {X : Type u_1} [TopologicalSpace X] {s : Set X} [DiscreteTopology ↑s] {x : X} (hx : x ∈ s) : ∃ (U : Set X), IsOpen U ∧ U ∩ s = {x}

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 disjoint_nhdsWithin_of_mem_discrete {X : Type u_1} [TopologicalSpace X] {s : Set X} [DiscreteTopology ↑s] {x : X} (hx : x ∈ s) : ∃ U ∈ nhdsWithin x {x}ᶜ, Disjoint U s

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 isClosedEmbedding_update {ι : Type u_3} {β : ι → Type u_4} [DecidableEq ι] [(i : ι) → TopologicalSpace (β i)] (x : (i : ι) → β i) (i : ι) [∀ (i : ι), T1Space (β i)] : Topology.IsClosedEmbedding (Function.update x i)

@[deprecated isClosedEmbedding_update (since := "2024-10-20")]

theorem closedEmbedding_update {ι : Type u_3} {β : ι → Type u_4} [DecidableEq ι] [(i : ι) → TopologicalSpace (β i)] (x : (i : ι) → β i) (i : ι) [∀ (i : ι), T1Space (β i)] : Topology.IsClosedEmbedding (Function.update x i)

Alias of isClosedEmbedding_update.

R₁ (preregular) spaces

class R1Space (X : Type u_3) [TopologicalSpace X] : Prop

A topological space is called a preregular (a.k.a. R₁) space, if any two topologically distinguishable points have disjoint neighbourhoods.

• specializes_or_disjoint_nhds (x y : X) : x ⤳ y ∨ Disjoint (nhds x) (nhds y)

Instances

• ContinuousMap.instR1Space
• ContinuousMapZero.instR1Space
• T2Space.r1Space
• instR1Space
• instR1SpaceForall
• instR1SpaceProd
• instR1SpaceSubtype

theorem r1Space_iff_specializes_or_disjoint_nhds (X : Type u_3) [TopologicalSpace X] : R1Space X ↔ ∀ (x y : X), x ⤳ y ∨ Disjoint (nhds x) (nhds y)

@[instance 100]

instance instR0Space {X : Type u_1} [TopologicalSpace X] [R1Space X] : R0Space X

theorem disjoint_nhds_nhds_iff_not_specializes {X : Type u_1} [TopologicalSpace X] [R1Space X] {x y : X} : Disjoint (nhds x) (nhds y) ↔ ¬x ⤳ y

theorem specializes_iff_not_disjoint {X : Type u_1} [TopologicalSpace X] [R1Space X] {x y : X} : x ⤳ y ↔ ¬Disjoint (nhds x) (nhds y)

theorem disjoint_nhds_nhds_iff_not_inseparable {X : Type u_1} [TopologicalSpace X] [R1Space X] {x y : X} : Disjoint (nhds x) (nhds y) ↔ ¬Inseparable x y

theorem r1Space_iff_inseparable_or_disjoint_nhds {X : Type u_3} [TopologicalSpace X] : R1Space X ↔ ∀ (x y : X), Inseparable x y ∨ Disjoint (nhds x) (nhds y)

theorem Inseparable.of_nhds_neBot {X : Type u_1} [TopologicalSpace X] [R1Space X] {x y : X} (h : (nhds x ⊓ nhds y).NeBot) : Inseparable x y

theorem tendsto_nhds_unique_inseparable {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] {f : Y → X} {l : Filter Y} {a b : X} [l.NeBot] (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto f l (nhds b)) : Inseparable a b

Limits are unique up to separability.

A weaker version of tendsto_nhds_unique for R1Space.

theorem isClosed_setOf_specializes {X : Type u_1} [TopologicalSpace X] [R1Space X] : IsClosed {p : X × X | p.1 ⤳ p.2}

theorem isClosed_setOf_inseparable {X : Type u_1} [TopologicalSpace X] [R1Space X] : IsClosed {p : X × X | Inseparable p.1 p.2}

theorem IsCompact.mem_closure_iff_exists_inseparable {X : Type u_1} [TopologicalSpace X] [R1Space X] {y : X} {K : Set X} (hK : IsCompact K) : y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y

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.closure_eq_biUnion_inseparable {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) : closure K = ⋃ x ∈ K, {y : X | Inseparable x y}

theorem IsCompact.closure_eq_biUnion_closure_singleton {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) : closure K = ⋃ x ∈ K, closure {x}

In an R₁ space, the closure of a compact set is the union of the closures of its points.

theorem IsCompact.closure_subset_of_isOpen {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) {U : Set X} (hU : IsOpen U) (hKU : K ⊆ U) : closure K ⊆ U

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 {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) : IsCompact (closure K)

The closure of a compact set in an R₁ space is a compact set.

theorem IsCompact.closure_of_subset {X : Type u_1} [TopologicalSpace X] [R1Space X] {s K : Set X} (hK : IsCompact K) (h : s ⊆ K) : IsCompact (closure s)

@[simp]

theorem exists_isCompact_superset_iff {X : Type u_1} [TopologicalSpace X] [R1Space X] {s : Set X} : (∃ (K : Set X), IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure s)

theorem SeparatedNhds.of_isCompact_isCompact_isClosed {X : Type u_1} [TopologicalSpace X] [R1Space X] {K L : Set X} (hK : IsCompact K) (hL : IsCompact L) (h'L : IsClosed L) (hd : Disjoint K L) : SeparatedNhds K L

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 IsCompact.binary_compact_cover {X : Type u_1} [TopologicalSpace X] [R1Space X] {K U V : Set X} (hK : IsCompact K) (hU : IsOpen U) (hV : IsOpen V) (h2K : K ⊆ U ∪ V) : ∃ (K₁ : Set X) (K₂ : Set X), IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

If a compact set is covered by two open sets, then we can cover it by two compact subsets.

theorem IsCompact.finite_compact_cover {X : Type u_1} [TopologicalSpace X] [R1Space X] {s : Set X} (hs : IsCompact s) {ι : Type u_3} (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

For every finite open cover Uᵢ of a compact set, there exists a compact cover Kᵢ ⊆ Uᵢ.

theorem R1Space.of_continuous_specializes_imp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace Y] {f : Y → X} (hc : Continuous f) (hspec : ∀ (x y : Y), f x ⤳ f y → x ⤳ y) : R1Space Y

theorem Topology.IsInducing.r1Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace Y] {f : Y → X} (hf : IsInducing f) : R1Space Y

@[deprecated Topology.IsInducing.r1Space (since := "2024-10-28")]

theorem Inducing.r1Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace Y] {f : Y → X} (hf : Topology.IsInducing f) : R1Space Y

Alias of Topology.IsInducing.r1Space.

theorem R1Space.induced {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] (f : Y → X) : R1Space Y

instance instR1SpaceSubtype {X : Type u_1} [TopologicalSpace X] [R1Space X] (p : X → Prop) : R1Space (Subtype p)

theorem R1Space.sInf {X : Type u_3} {T : Set (TopologicalSpace X)} (hT : ∀ t ∈ T, R1Space X) : R1Space X

theorem R1Space.iInf {ι : Type u_3} {X : Type u_4} {t : ι → TopologicalSpace X} (ht : ∀ (i : ι), R1Space X) : R1Space X

theorem R1Space.inf {X : Type u_3} {t₁ t₂ : TopologicalSpace X} (h₁ : R1Space X) (h₂ : R1Space X) : R1Space X

instance instR1SpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace Y] [R1Space Y] : R1Space (X × Y)

instance instR1SpaceForall {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), R1Space (X i)] : R1Space ((i : ι) → X i)

theorem exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [R1Space Y] {f : X → Y} {x : X} {K : Set X} {s : Set Y} (hf : Continuous f) (hs : s ∈ nhds (f x)) (hKc : IsCompact K) (hKx : K ∈ nhds x) : ∃ L ∈ nhds x, IsCompact L ∧ Set.MapsTo f L s

@[instance 900]

instance instLocallyCompactPairOfWeaklyLocallyCompactSpaceOfR1Space {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [TopologicalSpace Y] [R1Space Y] : LocallyCompactPair X Y

theorem IsCompact.isCompact_isClosed_basis_nhds {X : Type u_1} [TopologicalSpace X] [R1Space X] {x : X} {L : Set X} (hLc : IsCompact L) (hxL : L ∈ nhds x) : (nhds x).HasBasis (fun (K : Set X) => K ∈ nhds x ∧ IsCompact K ∧ IsClosed K) fun (x : Set X) => x

If a point in an R₁ space has a compact neighborhood, then it has a basis of compact closed neighborhoods.

@[simp]

theorem Filter.coclosedCompact_eq_cocompact {X : Type u_1} [TopologicalSpace X] [R1Space X] : coclosedCompact X = cocompact X

In an R₁ space, the filters coclosedCompact and cocompact are equal.

@[simp]

theorem Bornology.relativelyCompact_eq_inCompact {X : Type u_1} [TopologicalSpace X] [R1Space X] : relativelyCompact X = inCompact X

In an R₁ space, the bornologies relativelyCompact and inCompact are equal.

Lemmas about a weakly locally compact R₁ space

In fact, a space with these properties is locally compact and regular. Some lemmas are formulated using the latter assumptions below.

theorem isCompact_isClosed_basis_nhds {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X) : (nhds x).HasBasis (fun (K : Set X) => K ∈ nhds x ∧ IsCompact K ∧ IsClosed K) fun (x : Set X) => x

In a (weakly) locally compact R₁ space, compact closed neighborhoods of a point x form a basis of neighborhoods of x.

theorem exists_mem_nhds_isCompact_isClosed {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X) : ∃ K ∈ nhds x, IsCompact K ∧ IsClosed K

In a (weakly) locally compact R₁ space, each point admits a compact closed neighborhood.

@[instance 80]

instance WeaklyLocallyCompactSpace.locallyCompactSpace {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] : LocallyCompactSpace X

A weakly locally compact R₁ space is locally compact.

theorem exists_isOpen_superset_and_isCompact_closure {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] {K : Set X} (hK : IsCompact K) : ∃ (V : Set X), IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)

In a weakly locally compact R₁ space, every compact set has an open neighborhood with compact closure.

theorem exists_isOpen_mem_isCompact_closure {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X) : ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)

In a weakly locally compact R₁ space, every point has an open neighborhood with compact closure.