# mathlib3documentation

topology.alexandroff

# The Alexandroff Compactification #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

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

## Main results #

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

## Tags #

one-point compactification, compactness

### Definition and basic properties #

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

def alexandroff (X : Type u_1) :
Type u_1

The Alexandroff extension of an arbitrary topological space X

Equations
Instances for alexandroff
@[protected, instance]
def alexandroff.has_repr {X : Type u_1} [has_repr X] :

The repr uses the notation from the alexandroff locale.

Equations
def alexandroff.infty {X : Type u_1} :

The point at infinity

Equations
@[protected, instance]
def alexandroff.has_coe_t {X : Type u_1} :
Equations
@[protected, instance]
def alexandroff.inhabited {X : Type u_1} :
Equations
@[protected, instance]
def alexandroff.fintype {X : Type u_1} [fintype X] :
Equations
@[protected, instance]
def alexandroff.infinite {X : Type u_1} [infinite X] :
theorem alexandroff.coe_injective {X : Type u_1} :
@[norm_cast]
theorem alexandroff.coe_eq_coe {X : Type u_1} {x y : X} :
x = y x = y
@[simp]
theorem alexandroff.coe_ne_infty {X : Type u_1} (x : X) :
@[simp]
theorem alexandroff.infty_ne_coe {X : Type u_1} (x : X) :
@[protected]
def alexandroff.rec {X : Type u_1} (C : Sort u_2) (h₁ : C alexandroff.infty) (h₂ : Π (x : X), C x) (z : alexandroff X) :
C z

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

Equations
• h₁ h₂ = option.rec h₁ h₂
@[simp]
@[simp]
@[simp]
theorem alexandroff.compl_range_coe {X : Type u_1} :
theorem alexandroff.compl_infty {X : Type u_1} :
theorem alexandroff.compl_image_coe {X : Type u_1} (s : set X) :
(coe '' s) =
theorem alexandroff.ne_infty_iff_exists {X : Type u_1} {x : alexandroff X} :
(y : X), y = x
@[protected, instance]
def alexandroff.can_lift {X : Type u_1} :
X coe (λ (x : ,
Equations
theorem alexandroff.infty_not_mem_image_coe {X : Type u_1} {s : set X} :
@[simp]
theorem alexandroff.coe_preimage_infty {X : Type u_1} :

### Topological space structure on alexandroff X#

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

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

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

@[protected, instance]
Equations
@[simp]
theorem alexandroff.is_open_image_coe {X : Type u_1} {s : set X} :
@[simp]
theorem alexandroff.is_closed_image_coe {X : Type u_1} {s : set X} :
def alexandroff.opens_of_compl {X : Type u_1} (s : set X) (h₁ : is_closed s) (h₂ : is_compact s) :

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

Equations
theorem alexandroff.infty_mem_opens_of_compl {X : Type u_1} {s : set X} (h₁ : is_closed s) (h₂ : is_compact s) :
@[continuity]
theorem alexandroff.continuous_coe {X : Type u_1}  :
theorem alexandroff.is_open_map_coe {X : Type u_1}  :
theorem alexandroff.is_open_range_coe {X : Type u_1}  :
theorem alexandroff.is_closed_infty {X : Type u_1}  :
theorem alexandroff.nhds_coe_eq {X : Type u_1} (x : X) :
= (nhds x)
theorem alexandroff.nhds_within_coe_image {X : Type u_1} (s : set X) (x : X) :
(coe '' s) = s)
theorem alexandroff.nhds_within_coe {X : Type u_1} (s : set (alexandroff X)) (x : X) :
s = (coe ⁻¹' s))
theorem alexandroff.comap_coe_nhds {X : Type u_1} (x : X) :
(nhds x) = nhds x
@[protected, instance]
def alexandroff.nhds_within_compl_coe_ne_bot {X : Type u_1} (x : X) [h : {x}).ne_bot] :

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

@[protected, instance]

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

@[protected, instance]
def alexandroff.nhds_within_compl_ne_bot {X : Type u_1} [ (x : X), {x}).ne_bot] (x : alexandroff X) :
{x}).ne_bot
theorem alexandroff.nhds_infty_eq {X : Type u_1}  :
theorem alexandroff.has_basis_nhds_infty {X : Type u_1}  :
(λ (s : set X), (λ (s : set X), {alexandroff.infty})
@[simp]
theorem alexandroff.comap_coe_nhds_infty {X : Type u_1}  :
theorem alexandroff.le_nhds_infty {X : Type u_1} {f : filter (alexandroff X)} :
(s : set X), f
theorem alexandroff.tendsto_nhds_infty' {X : Type u_1} {α : Type u_2} {f : α} {l : filter α} :
theorem alexandroff.tendsto_nhds_infty {X : Type u_1} {α : Type u_2} {f : α} {l : filter α} :
(s : set α), s l (t : set X), set.maps_to (f coe) t s)
theorem alexandroff.continuous_at_infty' {X : Type u_1} {Y : Type u_2} {f : Y} :
theorem alexandroff.continuous_at_infty {X : Type u_1} {Y : Type u_2} {f : Y} :
(s : set Y), s ( (t : set X), set.maps_to (f coe) t s)
theorem alexandroff.continuous_at_coe {X : Type u_1} {Y : Type u_2} {f : Y} {x : X} :
theorem alexandroff.dense_range_coe {X : Type u_1}  :

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

@[simp]
theorem alexandroff.specializes_coe {X : Type u_1} {x y : X} :
x y x y
@[simp]
theorem alexandroff.inseparable_coe {X : Type u_1} {x y : X} :
y
theorem alexandroff.not_specializes_infty_coe {X : Type u_1} {x : X} :
theorem alexandroff.not_inseparable_infty_coe {X : Type u_1} {x : X} :
theorem alexandroff.not_inseparable_coe_infty {X : Type u_1} {x : X} :
theorem alexandroff.inseparable_iff {X : Type u_1} {x y : alexandroff X} :
y (x' : X), x = x' (y' : X), y = y' y'

### Compactness and separation properties #

In this section we prove that alexandroff 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 alexandroff X is a normal (hence, T₃ and Hausdorff) space.

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

@[protected, instance]
def alexandroff.compact_space {X : Type u_1}  :

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

@[protected, instance]
def alexandroff.t0_space {X : Type u_1} [t0_space X] :

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

@[protected, instance]
def alexandroff.t1_space {X : Type u_1} [t1_space X] :

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

@[protected, instance]
def alexandroff.normal_space {X : Type u_1} [t2_space X] :

The one point compactification of a locally compact Hausdorff space is a normal (hence, Hausdorff and regular) topological space.

@[protected, instance]
def alexandroff.connected_space {X : Type u_1}  :

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

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

A concrete counterexample shows that continuous.homeo_of_equiv_compact_to_t2 cannot be generalized from t2_space to t1_space.

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