mathlib documentation

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 #

Main results #

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_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 : alexandroff XSort u_2) (h₁ : C ) (h₂ : Π (x : X), C x) (z : alexandroff X) :
C z

Recursor for alexandroff using the preferred forms and ↑x.

Equations
@[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) :
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} :
Equations
theorem alexandroff.not_mem_range_coe_iff {X : Type u_1} {x : alexandroff X} :
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

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.

@[simp]
theorem alexandroff.is_open_image_coe {X : Type u_1} [topological_space X] {s : set X} :
@[simp]
def alexandroff.opens_of_compl {X : Type u_1} [topological_space X] (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} [topological_space X] {s : set X} (h₁ : is_closed s) (h₂ : is_compact s) :
theorem alexandroff.nhds_coe_eq {X : Type u_1} [topological_space X] (x : X) :
theorem alexandroff.nhds_within_coe_image {X : Type u_1} [topological_space X] (s : set X) (x : X) :
theorem alexandroff.nhds_within_coe {X : Type u_1} [topological_space X] (s : set (alexandroff X)) (x : X) :
theorem alexandroff.comap_coe_nhds {X : Type u_1} [topological_space X] (x : X) :
@[instance]

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

@[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} [topological_space X] [∀ (x : X), (𝓝[{x}] x).ne_bot] [(filter.cocompact X).ne_bot] (x : alexandroff X) :
theorem alexandroff.has_basis_nhds_infty {X : Type u_1} [topological_space X] :
(𝓝 ).has_basis (λ (s : set X), is_closed s is_compact s) (λ (s : set X), coe '' s {})
theorem alexandroff.le_nhds_infty {X : Type u_1} [topological_space X] {f : filter (alexandroff X)} :
f 𝓝 ∀ (s : set X), is_closed sis_compact scoe '' s {} f
theorem alexandroff.ultrafilter_le_nhds_infty {X : Type u_1} [topological_space X] {f : ultrafilter (alexandroff X)} :
f 𝓝 ∀ (s : set X), is_closed sis_compact scoe '' s f
theorem alexandroff.tendsto_nhds_infty' {X : Type u_1} [topological_space X] {α : Type u_2} {f : alexandroff X → α} {l : filter α} :
theorem alexandroff.tendsto_nhds_infty {X : Type u_1} [topological_space X] {α : Type u_2} {f : alexandroff X → α} {l : filter α} :
filter.tendsto f (𝓝 ) l ∀ (s : set α), s l(f s ∃ (t : set X), is_closed t is_compact t set.maps_to (f coe) t s)
theorem alexandroff.continuous_at_infty {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : alexandroff X → Y} :
continuous_at f ∀ (s : set Y), s 𝓝 (f )(∃ (t : set X), is_closed t is_compact t set.maps_to (f coe) t s)
theorem alexandroff.continuous_at_coe {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : alexandroff X → Y} {x : X} :

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

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]

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

@[instance]

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

@[instance]

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

@[instance]

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

@[instance]

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