# mathlibdocumentation

topology.alexandroff

# The Alexandroff Compactification #

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
def alexandroff.infty {X : Type u_1} :

The point at infinity

Equations
@[instance]
def alexandroff.has_coe_t {X : Type u_1} :
Equations
@[instance]
def alexandroff.inhabited {X : Type u_1} :
Equations
theorem alexandroff.coe_injective {X : Type u_1} :
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) :
def alexandroff.rec {X : Type u_1} (C : Sort u_2) (h₁ : C ) (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₂
theorem alexandroff.is_compl_range_coe_infty {X : Type u_1} :
{}
@[simp]
theorem alexandroff.range_coe_union_infty {X : Type u_1} :
@[simp]
theorem alexandroff.range_coe_inter_infty {X : Type u_1} :
@[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} :
x ∃ (y : X), y = x
@[instance]
def alexandroff.can_lift {X : Type u_1} :
X
Equations
theorem alexandroff.not_mem_range_coe_iff {X : Type u_1} {x : alexandroff X} :
x =
theorem alexandroff.infty_not_mem_range_coe {X : Type u_1} :
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.

@[instance]
def alexandroff.topological_space {X : Type u_1}  :
Equations
theorem alexandroff.is_open_def {X : Type u_1} {s : set (alexandroff X)} :
theorem alexandroff.is_open_iff_of_not_mem {X : Type u_1} {s : set (alexandroff X)} (h : s) :
theorem alexandroff.is_closed_iff_of_mem {X : Type u_1} {s : set (alexandroff X)} (h : s) :
@[simp]
theorem alexandroff.is_open_image_coe {X : Type u_1} {s : set X} :
theorem alexandroff.is_open_compl_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) :
h₂
theorem alexandroff.continuous_coe {X : Type u_1}  :
theorem alexandroff.is_open_map_coe {X : Type u_1}  :
theorem alexandroff.open_embedding_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) :
𝓝 x = (𝓝 x)
theorem alexandroff.nhds_within_coe_image {X : Type u_1} (s : set X) (x : X) :
theorem alexandroff.nhds_within_coe {X : Type u_1} (s : set (alexandroff X)) (x : X) :
theorem alexandroff.comap_coe_nhds {X : Type u_1} (x : X) :
(𝓝 x) = 𝓝 x
@[instance]
def alexandroff.nhds_within_compl_coe_ne_bot {X : Type u_1} (x : X) [h : (𝓝[{x}] x).ne_bot] :

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

theorem alexandroff.nhds_within_compl_infty_eq {X : Type u_1}  :
@[instance]

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

@[instance]
def alexandroff.nhds_within_compl_ne_bot {X : Type u_1} [∀ (x : X), (𝓝[{x}] x).ne_bot] [.ne_bot] (x : alexandroff X) :
theorem alexandroff.nhds_infty_eq {X : Type u_1}  :
theorem alexandroff.has_basis_nhds_infty {X : Type u_1}  :
(𝓝 ).has_basis (λ (s : set X), (λ (s : set X), {})
@[simp]
theorem alexandroff.comap_coe_nhds_infty {X : Type u_1}  :
theorem alexandroff.le_nhds_infty {X : Type u_1} {f : filter (alexandroff X)} :
f ∀ (s : set X), {} f
theorem alexandroff.ultrafilter_le_nhds_infty {X : Type u_1} {f : ultrafilter (alexandroff X)} :
f ∀ (s : set X), f
theorem alexandroff.tendsto_nhds_infty' {X : Type u_1} {α : Type u_2} {f : → α} {l : filter α} :
(𝓝 ) l (pure ) l l
theorem alexandroff.tendsto_nhds_infty {X : Type u_1} {α : Type u_2} {f : → α} {l : filter α} :
(𝓝 ) l ∀ (s : set α), s l(f s ∃ (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} :
(𝓝 (f ))
theorem alexandroff.continuous_at_infty {X : Type u_1} {Y : Type u_2} {f : → Y} :
∀ (s : set Y), s 𝓝 (f )(∃ (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} [.ne_bot] :

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

theorem alexandroff.dense_embedding_coe {X : Type u_1} [.ne_bot] :

### 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, regular and Hausdorff) space.

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

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

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

@[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.

@[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.

@[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.

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

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