Documentation

Mathlib.Topology.Compactification.OnePoint

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} :

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) :

@[simp]

theorem OnePoint.infty_ne_coe {X : Type u_1} (x : 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] :

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.