The OnePoint Compactification

We construct the OnePoint compactification (the one-point compactification) of an arbitrary topological space X and prove some properties inherited from X.

Main definitions

• OnePoint: the OnePoint compactification, we use coercion for the canonical embedding X → OnePoint X; when X is already compact, the compactification adds an isolated point to the space.
• OnePoint.infty: the extra point

Main results

• The topological structure of OnePoint X
• The connectedness of OnePoint X for a noncompact, preconnected X
• OnePoint X is T₀ for a T₀ space X
• OnePoint X is T₁ for a T₁ space X
• OnePoint X is normal if X is a locally compact Hausdorff space

Tags

one-point compactification, Alexandroff compactification, compactness

Definition and basic properties

In this section we define OnePoint X to be the disjoint union of X and ∞, implemented as Option X. Then we restate some lemmas about Option X for OnePoint X.

def OnePoint (X : Type u_3) : Type u_3

The OnePoint extension of an arbitrary topological space X

Equations

• OnePoint X = Option X

instance instReprOnePoint {X : Type u_1} [Repr X] : Repr (OnePoint X)

The repr uses the notation from the OnePoint locale.

Equations

• instReprOnePoint = { reprPrec := fun (o : OnePoint X) (x : ℕ) => match o with | none => Std.Format.text "∞" | some a => Std.Format.text "↑" ++ repr a }

@[match_pattern]

def OnePoint.infty {X : Type u_1} : OnePoint X

The point at infinity

Equations

• OnePoint.infty = none

def OnePoint.«term∞» : Lean.ParserDescr

The point at infinity

Equations

• OnePoint.«term∞» = Lean.ParserDescr.node `OnePoint.«term∞» 1024 (Lean.ParserDescr.symbol "∞")

@[match_pattern]

def OnePoint.some {X : Type u_1} : X → OnePoint X

Coercion from X to OnePoint X.

Equations

• OnePoint.some = some

@[simp]

theorem OnePoint.some_eq_iff {X : Type u_1} (x₁ x₂ : X) : ↑x₁ = ↑x₂ ↔ x₁ = x₂

instance OnePoint.instCoeTC {X : Type u_1} : CoeTC X (OnePoint X)

Equations

• OnePoint.instCoeTC = { coe := OnePoint.some }

instance OnePoint.instInhabited {X : Type u_1} : Inhabited (OnePoint X)

Equations

• OnePoint.instInhabited = { default := OnePoint.infty }

theorem OnePoint.forall {X : Type u_1} {p : OnePoint X → Prop} : (∀ (x : OnePoint X), p x) ↔ p infty ∧ ∀ (x : X), p ↑x

theorem OnePoint.exists {X : Type u_1} {p : OnePoint X → Prop} : (∃ (x : OnePoint X), p x) ↔ p infty ∨ ∃ (x : X), p ↑x

instance OnePoint.instFintype {X : Type u_1} [Fintype X] : Fintype (OnePoint X)

Equations

• OnePoint.instFintype = inferInstanceAs (Fintype (Option X))

instance OnePoint.infinite {X : Type u_1} [Infinite X] : Infinite (OnePoint X)

theorem OnePoint.coe_injective {X : Type u_1} : Function.Injective some

theorem OnePoint.coe_eq_coe {X : Type u_1} {x y : X} : ↑x = ↑y ↔ x = y

@[simp]

theorem OnePoint.coe_ne_infty {X : Type u_1} (x : X) : ↑x ≠ infty

@[simp]

theorem OnePoint.infty_ne_coe {X : Type u_1} (x : X) : infty ≠ ↑x

def OnePoint.rec {X : Type u_1} {C : OnePoint X → Sort u_3} (infty : C infty) (coe : (x : X) → C ↑x) (z : OnePoint X) : C z

Recursor for OnePoint using the preferred forms ∞ and ↑x.

Equations

• OnePoint.rec infty coe none = infty
• OnePoint.rec infty coe (some a) = coe a

@[inline]

def OnePoint.elim {X : Type u_1} {Y : Type u_2} : OnePoint X → Y → (X → Y) → Y

An elimination principle for OnePoint.

Equations

• OnePoint.elim = Option.elim

@[simp]

theorem OnePoint.elim_infty {X : Type u_1} {Y : Type u_2} (y : Y) (f : X → Y) : infty.elim y f = y

@[simp]

theorem OnePoint.elim_some {X : Type u_1} {Y : Type u_2} (y : Y) (f : X → Y) (x : X) : (↑x).elim y f = f x

theorem OnePoint.isCompl_range_coe_infty {X : Type u_1} : IsCompl (Set.range some) {infty}

theorem OnePoint.range_coe_union_infty {X : Type u_1} : Set.range some ∪ {infty} = Set.univ

@[simp]

theorem OnePoint.insert_infty_range_coe {X : Type u_1} : insert infty (Set.range some) = Set.univ

@[simp]

theorem OnePoint.range_coe_inter_infty {X : Type u_1} : Set.range some ∩ {infty} = ∅

@[simp]

theorem OnePoint.compl_range_coe {X : Type u_1} : (Set.range some)ᶜ = {infty}

theorem OnePoint.compl_infty {X : Type u_1} : {infty}ᶜ = Set.range some

theorem OnePoint.compl_image_coe {X : Type u_1} (s : Set X) : (some '' s)ᶜ = some '' sᶜ ∪ {infty}

theorem OnePoint.ne_infty_iff_exists {X : Type u_1} {x : OnePoint X} : x ≠ infty ↔ ∃ (y : X), ↑y = x

instance OnePoint.canLift {X : Type u_1} : CanLift (OnePoint X) X some fun (x : OnePoint X) => x ≠ infty

theorem OnePoint.notMem_range_coe_iff {X : Type u_1} {x : OnePoint X} : x ∉ Set.range some ↔ x = infty

@[deprecated OnePoint.notMem_range_coe_iff (since := "2025-05-23")]

theorem OnePoint.not_mem_range_coe_iff {X : Type u_1} {x : OnePoint X} : x ∉ Set.range some ↔ x = infty

Alias of OnePoint.notMem_range_coe_iff.

theorem OnePoint.infty_notMem_range_coe {X : Type u_1} : infty ∉ Set.range some

@[deprecated OnePoint.infty_notMem_range_coe (since := "2025-05-23")]

theorem OnePoint.infty_not_mem_range_coe {X : Type u_1} : infty ∉ Set.range some

Alias of OnePoint.infty_notMem_range_coe.

theorem OnePoint.infty_notMem_image_coe {X : Type u_1} {s : Set X} : infty ∉ some '' s

@[deprecated OnePoint.infty_notMem_image_coe (since := "2025-05-23")]

theorem OnePoint.infty_not_mem_image_coe {X : Type u_1} {s : Set X} : infty ∉ some '' s

Alias of OnePoint.infty_notMem_image_coe.

@[simp]

theorem OnePoint.coe_preimage_infty {X : Type u_1} : some ⁻¹' {infty} = ∅

def OnePoint.map {X : Type u_1} {Y : Type u_2} (f : X → Y) : OnePoint X → OnePoint Y

Extend a map f : X → Y to a map OnePoint X → OnePoint Y by sending infinity to infinity.

Equations

• OnePoint.map f = Option.map f

@[simp]

theorem OnePoint.map_infty {X : Type u_1} {Y : Type u_2} (f : X → Y) : OnePoint.map f infty = infty

@[simp]

theorem OnePoint.map_some {X : Type u_1} {Y : Type u_2} (f : X → Y) (x : X) : OnePoint.map f ↑x = ↑(f x)

@[simp]

theorem OnePoint.map_id {X : Type u_1} : OnePoint.map id = id

theorem OnePoint.map_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (g : X → Y) : OnePoint.map (f ∘ g) = OnePoint.map f ∘ OnePoint.map g

Topological space structure on OnePoint X

We define a topological space structure on OnePoint X so that s is open if and only if

• (↑) ⁻¹' s is open in X;
• if ∞ ∈ s, then ((↑) ⁻¹' s)ᶜ is compact.

Then we reformulate this definition in a few different ways, and prove that (↑) : X → OnePoint X is an open embedding. If X is not a compact space, then we also prove that (↑) has dense range, so it is a dense embedding.

instance OnePoint.instTopologicalSpace {X : Type u_1} [TopologicalSpace X] : TopologicalSpace (OnePoint X)

Equations

• One or more equations did not get rendered due to their size.

theorem OnePoint.isOpen_def {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} : IsOpen s ↔ (infty ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)

theorem OnePoint.isOpen_iff_of_mem' {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : infty ∈ s) : IsOpen s ↔ IsCompact (some ⁻¹' s)ᶜ ∧ IsOpen (some ⁻¹' s)

theorem OnePoint.isOpen_iff_of_mem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : infty ∈ s) : IsOpen s ↔ IsClosed (some ⁻¹' s)ᶜ ∧ IsCompact (some ⁻¹' s)ᶜ

theorem OnePoint.isOpen_iff_of_notMem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : infty ∉ s) : IsOpen s ↔ IsOpen (some ⁻¹' s)

@[deprecated OnePoint.isOpen_iff_of_notMem (since := "2025-05-23")]

theorem OnePoint.isOpen_iff_of_not_mem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : infty ∉ s) : IsOpen s ↔ IsOpen (some ⁻¹' s)

Alias of OnePoint.isOpen_iff_of_notMem.

theorem OnePoint.isClosed_iff_of_mem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : infty ∈ s) : IsClosed s ↔ IsClosed (some ⁻¹' s)

theorem OnePoint.isClosed_iff_of_notMem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : infty ∉ s) : IsClosed s ↔ IsClosed (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)

@[deprecated OnePoint.isClosed_iff_of_notMem (since := "2025-05-23")]

theorem OnePoint.isClosed_iff_of_not_mem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : infty ∉ s) : IsClosed s ↔ IsClosed (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)

Alias of OnePoint.isClosed_iff_of_notMem.

@[simp]

theorem OnePoint.isOpen_image_coe {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsOpen (some '' s) ↔ IsOpen s

theorem OnePoint.isOpen_compl_image_coe {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsOpen (some '' s)ᶜ ↔ IsClosed s ∧ IsCompact s

@[simp]

theorem OnePoint.isClosed_image_coe {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsClosed (some '' s) ↔ IsClosed s ∧ IsCompact s

def OnePoint.opensOfCompl {X : Type u_1} [TopologicalSpace X] (s : Set X) (h₁ : IsClosed s) (h₂ : IsCompact s) : TopologicalSpace.Opens (OnePoint X)

An open set in OnePoint X constructed from a closed compact set in X

Equations

• OnePoint.opensOfCompl s h₁ h₂ = { carrier := (OnePoint.some '' s)ᶜ, is_open' := ⋯ }

theorem OnePoint.infty_mem_opensOfCompl {X : Type u_1} [TopologicalSpace X] {s : Set X} (h₁ : IsClosed s) (h₂ : IsCompact s) : infty ∈ opensOfCompl s h₁ h₂

theorem OnePoint.continuous_coe {X : Type u_1} [TopologicalSpace X] : Continuous some

theorem OnePoint.isOpenMap_coe {X : Type u_1} [TopologicalSpace X] : IsOpenMap some

theorem OnePoint.isOpenEmbedding_coe {X : Type u_1} [TopologicalSpace X] : Topology.IsOpenEmbedding some

theorem OnePoint.isOpen_range_coe {X : Type u_1} [TopologicalSpace X] : IsOpen (Set.range some)

theorem OnePoint.isClosed_infty {X : Type u_1} [TopologicalSpace X] : IsClosed {infty}

theorem OnePoint.nhds_coe_eq {X : Type u_1} [TopologicalSpace X] (x : X) : nhds ↑x = Filter.map some (nhds x)

theorem OnePoint.nhdsWithin_coe_image {X : Type u_1} [TopologicalSpace X] (s : Set X) (x : X) : nhdsWithin (↑x) (some '' s) = Filter.map some (nhdsWithin x s)

theorem OnePoint.nhdsWithin_coe {X : Type u_1} [TopologicalSpace X] (s : Set (OnePoint X)) (x : X) : nhdsWithin (↑x) s = Filter.map some (nhdsWithin x (some ⁻¹' s))

theorem OnePoint.comap_coe_nhds {X : Type u_1} [TopologicalSpace X] (x : X) : Filter.comap some (nhds ↑x) = nhds x

instance OnePoint.nhdsNE_coe_neBot {X : Type u_1} [TopologicalSpace X] (x : X) [h : (nhdsWithin x {x}ᶜ).NeBot] : (nhdsWithin ↑x {↑x}ᶜ).NeBot

If x is not an isolated point of X, then x : OnePoint X is not an isolated point of OnePoint X.

@[deprecated OnePoint.nhdsNE_coe_neBot (since := "2025-03-02")]

theorem OnePoint.nhdsWithin_compl_coe_neBot {X : Type u_1} [TopologicalSpace X] (x : X) [h : (nhdsWithin x {x}ᶜ).NeBot] : (nhdsWithin ↑x {↑x}ᶜ).NeBot

Alias of OnePoint.nhdsNE_coe_neBot.

---

If x is not an isolated point of X, then x : OnePoint X is not an isolated point of OnePoint X.

theorem OnePoint.nhdsNE_infty_eq {X : Type u_1} [TopologicalSpace X] : nhdsWithin infty {infty}ᶜ = Filter.map some (Filter.coclosedCompact X)

@[deprecated OnePoint.nhdsNE_infty_eq (since := "2025-03-02")]

theorem OnePoint.nhdsWithin_compl_infty_eq {X : Type u_1} [TopologicalSpace X] : nhdsWithin infty {infty}ᶜ = Filter.map some (Filter.coclosedCompact X)

Alias of OnePoint.nhdsNE_infty_eq.

instance OnePoint.nhdsNE_infty_neBot {X : Type u_1} [TopologicalSpace X] [NoncompactSpace X] : (nhdsWithin infty {infty}ᶜ).NeBot

If X is a non-compact space, then ∞ is not an isolated point of OnePoint X.

@[deprecated OnePoint.nhdsNE_infty_neBot (since := "2025-03-02")]

theorem OnePoint.nhdsWithin_compl_infty_neBot {X : Type u_1} [TopologicalSpace X] [NoncompactSpace X] : (nhdsWithin infty {infty}ᶜ).NeBot

Alias of OnePoint.nhdsNE_infty_neBot.

---

If X is a non-compact space, then ∞ is not an isolated point of OnePoint X.

@[instance 900]

instance OnePoint.nhdsNE_neBot {X : Type u_1} [TopologicalSpace X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] [NoncompactSpace X] (x : OnePoint X) : (nhdsWithin x {x}ᶜ).NeBot

@[deprecated OnePoint.nhdsNE_neBot (since := "2025-03-02")]

theorem OnePoint.nhdsWithin_compl_neBot {X : Type u_1} [TopologicalSpace X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] [NoncompactSpace X] (x : OnePoint X) : (nhdsWithin x {x}ᶜ).NeBot

Alias of OnePoint.nhdsNE_neBot.

theorem OnePoint.nhds_infty_eq {X : Type u_1} [TopologicalSpace X] : nhds infty = Filter.map some (Filter.coclosedCompact X) ⊔ pure infty

theorem OnePoint.tendsto_coe_infty {X : Type u_1} [TopologicalSpace X] : Filter.Tendsto some (Filter.coclosedCompact X) (nhds infty)

theorem OnePoint.hasBasis_nhds_infty {X : Type u_1} [TopologicalSpace X] : (nhds infty).HasBasis (fun (s : Set X) => IsClosed s ∧ IsCompact s) fun (s : Set X) => some '' sᶜ ∪ {infty}

@[simp]

theorem OnePoint.comap_coe_nhds_infty {X : Type u_1} [TopologicalSpace X] : Filter.comap some (nhds infty) = Filter.coclosedCompact X

theorem OnePoint.le_nhds_infty {X : Type u_1} [TopologicalSpace X] {f : Filter (OnePoint X)} : f ≤ nhds infty ↔ ∀ (s : Set X), IsClosed s → IsCompact s → some '' sᶜ ∪ {infty} ∈ f

theorem OnePoint.ultrafilter_le_nhds_infty {X : Type u_1} [TopologicalSpace X] {f : Ultrafilter (OnePoint X)} : ↑f ≤ nhds infty ↔ ∀ (s : Set X), IsClosed s → IsCompact s → some '' s ∉ f

theorem OnePoint.tendsto_nhds_infty' {X : Type u_1} [TopologicalSpace X] {α : Type u_3} {f : OnePoint X → α} {l : Filter α} : Filter.Tendsto f (nhds infty) l ↔ Filter.Tendsto f (pure infty) l ∧ Filter.Tendsto (f ∘ some) (Filter.coclosedCompact X) l

theorem OnePoint.tendsto_nhds_infty {X : Type u_1} [TopologicalSpace X] {α : Type u_3} {f : OnePoint X → α} {l : Filter α} : Filter.Tendsto f (nhds infty) l ↔ ∀ s ∈ l, f infty ∈ s ∧ ∃ (t : Set X), IsClosed t ∧ IsCompact t ∧ Set.MapsTo (f ∘ some) tᶜ s

theorem OnePoint.continuousAt_infty' {X : Type u_1} [TopologicalSpace X] {Y : Type u_3} [TopologicalSpace Y] {f : OnePoint X → Y} : ContinuousAt f infty ↔ Filter.Tendsto (f ∘ some) (Filter.coclosedCompact X) (nhds (f infty))

theorem OnePoint.continuousAt_infty {X : Type u_1} [TopologicalSpace X] {Y : Type u_3} [TopologicalSpace Y] {f : OnePoint X → Y} : ContinuousAt f infty ↔ ∀ s ∈ nhds (f infty), ∃ (t : Set X), IsClosed t ∧ IsCompact t ∧ Set.MapsTo (f ∘ some) tᶜ s

theorem OnePoint.continuousAt_coe {X : Type u_1} [TopologicalSpace X] {Y : Type u_3} [TopologicalSpace Y] {f : OnePoint X → Y} {x : X} : ContinuousAt f ↑x ↔ ContinuousAt (f ∘ some) x

theorem OnePoint.continuous_iff {X : Type u_1} [TopologicalSpace X] {Y : Type u_3} [TopologicalSpace Y] (f : OnePoint X → Y) : Continuous f ↔ Filter.Tendsto (fun (x : X) => f ↑x) (Filter.coclosedCompact X) (nhds (f infty)) ∧ Continuous fun (x : X) => f ↑x

def OnePoint.continuousMapMk {X : Type u_1} [TopologicalSpace X] {Y : Type u_3} [TopologicalSpace Y] (f : C(X, Y)) (y : Y) (h : Filter.Tendsto (⇑f) (Filter.coclosedCompact X) (nhds y)) : C(OnePoint X, Y)

A constructor for continuous maps out of a one point compactification, given a continuous map from the underlying space and a limit value at infinity.

Equations

• OnePoint.continuousMapMk f y h = { toFun := fun (x : OnePoint X) => x.elim y ⇑f, continuous_toFun := ⋯ }

theorem OnePoint.continuous_iff_from_discrete {X : Type u_1} [TopologicalSpace X] {Y : Type u_3} [TopologicalSpace Y] [DiscreteTopology X] (f : OnePoint X → Y) : Continuous f ↔ Filter.Tendsto (fun (x : X) => f ↑x) Filter.cofinite (nhds (f infty))

def OnePoint.continuousMapMkDiscrete {X : Type u_1} [TopologicalSpace X] {Y : Type u_3} [TopologicalSpace Y] [DiscreteTopology X] (f : X → Y) (y : Y) (h : Filter.Tendsto f Filter.cofinite (nhds y)) : C(OnePoint X, Y)

A constructor for continuous maps out of a one point compactification of a discrete space, given a map from the underlying space and a limit value at infinity.

Equations

• OnePoint.continuousMapMkDiscrete f y h = OnePoint.continuousMapMk { toFun := f, continuous_toFun := ⋯ } y ⋯

noncomputable def OnePoint.continuousMapDiscreteEquiv (X : Type u_1) [TopologicalSpace X] (Y : Type u_3) [DiscreteTopology X] [TopologicalSpace Y] [T2Space Y] [Infinite X] : C(OnePoint X, Y) ≃ { f : X → Y // ∃ (L : Y), Filter.Tendsto (fun (x : X) => f x) Filter.cofinite (nhds L) }

Continuous maps out of the one point compactification of an infinite discrete space to a Hausdorff space correspond bijectively to "convergent" maps out of the discrete space.

Equations

• One or more equations did not get rendered due to their size.

theorem OnePoint.continuous_iff_from_nat {Y : Type u_3} [TopologicalSpace Y] (f : OnePoint ℕ → Y) : Continuous f ↔ Filter.Tendsto (fun (x : ℕ) => f ↑x) Filter.atTop (nhds (f infty))

def OnePoint.continuousMapMkNat {Y : Type u_3} [TopologicalSpace Y] (f : ℕ → Y) (y : Y) (h : Filter.Tendsto f Filter.atTop (nhds y)) : C(OnePoint ℕ, Y)

A constructor for continuous maps out of the one point compactification of ℕ, given a sequence and a limit value at infinity.

Equations

• OnePoint.continuousMapMkNat f y h = OnePoint.continuousMapMkDiscrete f y ⋯

noncomputable def OnePoint.continuousMapNatEquiv (Y : Type u_3) [TopologicalSpace Y] [T2Space Y] : C(OnePoint ℕ, Y) ≃ { f : ℕ → Y // ∃ (L : Y), Filter.Tendsto (fun (x : ℕ) => f x) Filter.atTop (nhds L) }

Continuous maps out of the one point compactification of ℕ to a Hausdorff space Y correspond bijectively to convergent sequences in Y.

Equations

• One or more equations did not get rendered due to their size.

theorem OnePoint.denseRange_coe {X : Type u_1} [TopologicalSpace X] [NoncompactSpace X] : DenseRange some

If X is not a compact space, then the natural embedding X → OnePoint X has dense range.

theorem OnePoint.isDenseEmbedding_coe {X : Type u_1} [TopologicalSpace X] [NoncompactSpace X] : IsDenseEmbedding some

@[simp]

theorem OnePoint.specializes_coe {X : Type u_1} [TopologicalSpace X] {x y : X} : ↑x ⤳ ↑y ↔ x ⤳ y

@[simp]

theorem OnePoint.inseparable_coe {X : Type u_1} [TopologicalSpace X] {x y : X} : Inseparable ↑x ↑y ↔ Inseparable x y

theorem OnePoint.not_specializes_infty_coe {X : Type u_1} [TopologicalSpace X] {x : X} : ¬infty ⤳ ↑x

theorem OnePoint.not_inseparable_infty_coe {X : Type u_1} [TopologicalSpace X] {x : X} : ¬Inseparable infty ↑x

theorem OnePoint.not_inseparable_coe_infty {X : Type u_1} [TopologicalSpace X] {x : X} : ¬Inseparable (↑x) infty

theorem OnePoint.inseparable_iff {X : Type u_1} [TopologicalSpace X] {x y : OnePoint X} : Inseparable x y ↔ x = infty ∧ y = infty ∨ ∃ (x' : X), x = ↑x' ∧ ∃ (y' : X), y = ↑y' ∧ Inseparable x' y'

theorem OnePoint.continuous_map_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : Continuous (OnePoint.map f) ↔ Continuous f ∧ Filter.Tendsto f (Filter.coclosedCompact X) (Filter.coclosedCompact Y)

theorem OnePoint.continuous_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hc : Continuous f) (h : Filter.Tendsto f (Filter.coclosedCompact X) (Filter.coclosedCompact Y)) : Continuous (OnePoint.map f)

Compactness and separation properties

In this section we prove that OnePoint X is a compact space; it is a T₀ (resp., T₁) space if the original space satisfies the same separation axiom. If the original space is a locally compact Hausdorff space, then OnePoint X is a normal (hence, T₃ and Hausdorff) space.

Finally, if the original space X is not compact and is a preconnected space, then OnePoint X is a connected space.

instance OnePoint.instCompactSpace {X : Type u_1} [TopologicalSpace X] : CompactSpace (OnePoint X)

For any topological space X, its one point compactification is a compact space.

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

The one point compactification of a T0Space space is a T0Space.

instance OnePoint.instT1Space {X : Type u_1} [TopologicalSpace X] [T1Space X] : T1Space (OnePoint X)

The one point compactification of a T1Space space is a T1Space.

instance OnePoint.instNormalSpaceOfWeaklyLocallyCompactSpaceOfR1Space {X : Type u_1} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [R1Space X] : NormalSpace (OnePoint X)

The one point compactification of a weakly locally compact R₁ space is a normal topological space.

instance OnePoint.instConnectedSpaceOfPreconnectedSpaceOfNoncompactSpace {X : Type u_1} [TopologicalSpace X] [PreconnectedSpace X] [NoncompactSpace X] : ConnectedSpace (OnePoint X)

If X is not a compact space, then OnePoint X is a connected space.

theorem OnePoint.not_continuous_cofiniteTopology_of_symm {X : Type u_1} [TopologicalSpace X] [Infinite X] [DiscreteTopology X] : ¬Continuous ⇑CofiniteTopology.of.symm

If X is an infinite type with discrete topology (e.g., ℕ), then the identity map from CofiniteTopology (OnePoint X) to OnePoint X is not continuous.

instance OnePoint.instTotallySeparatedSpaceOfDiscreteTopology (X : Type u_3) [TopologicalSpace X] [DiscreteTopology X] : TotallySeparatedSpace (OnePoint X)

noncomputable def OnePoint.equivOfIsEmbeddingOfRangeEq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] (y : Y) (f : X → Y) (hf : Topology.IsEmbedding f) (hy : Set.range f = {y}ᶜ) : OnePoint X ≃ₜ Y

If f embeds X into a compact Hausdorff space Y, and has exactly one point outside its range, then (Y, f) is the one-point compactification of X.

Equations

• OnePoint.equivOfIsEmbeddingOfRangeEq y f hf hy = ⋯.homeoOfEquivCompactToT2

@[simp]

theorem OnePoint.equivOfIsEmbeddingOfRangeEq_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] (y : Y) (f : X → Y) (hf : Topology.IsEmbedding f) (hy : Set.range f = {y}ᶜ) (x : X) : (equivOfIsEmbeddingOfRangeEq y f hf hy) ↑x = f x

@[simp]

theorem OnePoint.equivOfIsEmbeddingOfRangeEq_apply_infty {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] (y : Y) (f : X → Y) (hf : Topology.IsEmbedding f) (hy : Set.range f = {y}ᶜ) : (equivOfIsEmbeddingOfRangeEq y f hf hy) infty = y

def Homeomorph.onePointCongr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : OnePoint X ≃ₜ OnePoint Y

Extend a homeomorphism of topological spaces to the homeomorphism of their one point compactifications.

Equations

• h.onePointCongr = { toFun := OnePoint.map ⇑h, invFun := OnePoint.map ⇑h.symm, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.onePointCongr_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (a✝ : OnePoint X) : h.onePointCongr a✝ = OnePoint.map (⇑h) a✝

@[simp]

theorem Homeomorph.onePointCongr_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (a✝ : OnePoint Y) : h.onePointCongr.symm a✝ = OnePoint.map (⇑h.symm) a✝

theorem Continuous.homeoOfEquivCompactToT2.t1_counterexample : ∃ (α : Type) (β : Type) (x : TopologicalSpace α) (x_1 : TopologicalSpace β), CompactSpace α ∧ T1Space β ∧ ∃ (f : α ≃ β), Continuous ⇑f ∧ ¬Continuous ⇑f.symm

A concrete counterexample shows that Continuous.homeoOfEquivCompactToT2 cannot be generalized from T2Space to T1Space.

Let α = OnePoint ℕ be the one-point compactification of ℕ, and let β be the same space OnePoint ℕ with the cofinite topology. Then α is compact, β is T1, and the identity map id : α → β is a continuous equivalence that is not a homeomorphism.