Theorems · Definition · general topology

OnePoint.continuousMapMkDiscrete

{X : Type u_1} →
  [inst : TopologicalSpace X] →
    {Y : Type u_3} →
      [inst_1 : TopologicalSpace Y] →
        [DiscreteTopology X] → (f : X → Y) → (y : Y) → 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.

Defined in

Mathlib.Topology.Compactification.OnePoint.Basic

Cited by

0 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceDiscreteTopology