Approach filters in the one-point compactification

The punctured neighbourhoods of a point of the space in its one-point compactification are the images of its punctured neighbourhoods in the space, so the inclusion preserves them.

Approaching infinity within the image of a set is described by the coclosed-compact filter restricted to that set. In a pseudometric space, escaping bounded sets gives convergence to the compactifying point. These facts translate limits in the original space into limits in its one-point compactification.

The one-point compactification of a proper pseudometric space is first countable: at a point of the space it inherits the neighbourhood filter of the space, and at infinity the complements of the closed balls about a fixed point form a countable basis. Being also compact, it is then sequentially compact, and Fatou-type limit arguments may be run along its neighbourhood filters. On a proper space the extended distance from a fixed point, with value ⊤ at infinity, is continuous on the one-point compactification.

theorem TauCeti.OnePoint.nhdsNE_coe_eq {X : Type u_1} [TopologicalSpace X] (x : X) : nhdsWithin ↑x {↑x}ᶜ = Filter.map OnePoint.some (nhdsWithin x {x}ᶜ)

The punctured neighbourhoods of a point of X in the one-point compactification are the images of its punctured neighbourhoods in X.

theorem TauCeti.OnePoint.tendsto_coe_nhdsNE {X : Type u_1} [TopologicalSpace X] (x : X) : Filter.Tendsto OnePoint.some (nhdsWithin x {x}ᶜ) (nhdsWithin ↑x {↑x}ᶜ)

The inclusion into the one-point compactification maps punctured neighbourhoods to punctured neighbourhoods.

theorem TauCeti.nhdsWithin_infty_coe_image {X : Type u_1} [TopologicalSpace X] (s : Set X) : nhdsWithin OnePoint.infty (OnePoint.some '' s) = Filter.map OnePoint.some (Filter.coclosedCompact X ⊓ Filter.principal s)

Approaching infinity within the image of a set in the one-point compactification is equivalent to escaping closed compact sets within the original set.

theorem TauCeti.tendsto_coe_infty_of_tendsto_cobounded {α : Type u_1} {X : Type u_2} [PseudoMetricSpace X] {f : α → X} {l : Filter α} (h : Filter.Tendsto f l (Bornology.cobounded X)) : Filter.Tendsto (fun (x : α) => ↑(f x)) l (nhds OnePoint.infty)

A map escaping bounded sets in a pseudometric space converges to the compactifying point after embedding in the one-point compactification.

instance TauCeti.instFirstCountableTopologyOnePointOfProperSpace_tauCeti {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] : FirstCountableTopology (OnePoint X)

The one-point compactification of a proper pseudometric space is first countable. In a proper space the coclosed-compact filter is the cobounded filter, which is the pullback of atTop along the distance to any fixed point.

theorem TauCeti.continuous_elim_edist {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] (x : X) : Continuous fun (b : OnePoint X) => b.elim ⊤ (edist x)

On a proper space, the extended distance from a fixed point to a point of the one-point compactification, with value ⊤ at infinity, is continuous.