Closed embedding of continuous paths

The inclusion of continuous paths into Skorokhod space is a closed embedding. Its topology is the uniform topology, and its range is closed because a uniform limit of continuous paths is continuous.

theorem BGW.Skorokhod.isClosedEmbedding_ofContinuous {T : ℝ} {E : Type u_1} [MetricSpace E] : Topology.IsClosedEmbedding ofContinuous

Continuous paths form a closed subset of D, on which J1 is the uniform topology (C5.3).