A locally uniform limit of continuous functions is continuous

A uniform limit of continuous functions is continuous

The type of bounded continuous functions from a topological space to a metric space

If a function is continuous on a compact space, it is automatically bounded, and therefore gives rise to an element of the type of bounded continuous functions

If a function is bounded on a discrete space, it is automatically continuous, and therefore gives rise to an element of the type of bounded continuous functions

The uniform distance between two bounded continuous functions

The pointwise distance is controlled by the distance between functions, by definition

The distance between two functions is controlled by the supremum of the pointwise distances

On an empty space, bounded continuous functions are at distance 0

The type of bounded continuous functions, with the uniform distance, is a metric space.

If the target space is inhabited, so is the space of bounded continuous functions

The evaluation map is continuous, as a joint function of u and x

In particular, when x is fixed, f → f x is continuous

When f is fixed, x → f x is also continuous, by definition

Bounded continuous functions taking values in a complete space form a complete space.

Composition (in the target) of a bounded continuous function with a Lipschitz map again gives a bounded continuous function

The composition operator (in the target) with a Lipschitz map is continuous

Restriction (in the target) of a bounded continuous function taking values in a subset

First version, with pointwise equicontinuity and range in a compact space

Second version, with pointwise equicontinuity and range in a compact subset

Third (main) version, with pointwise equicontinuity and range in a compact subset, but without closedness. The closure is then compact

The norm of a function is controlled by the supremum of the pointwise norms

The pointwise sum of two bounded continuous functions is again bounded continuous.

The pointwise opposite of a bounded continuous function is again bounded continuous.

Constructing a bounded continuous function from a uniformly bounded continuous function taking values in a normed group.

Constructing a bounded continuous function from a uniformly bounded function on a discrete space, taking values in a normed group