Separability of the Skorokhod space #
Finite small-oscillation partitions are encoded by countably many time-value labels. The partition matching estimate controls the diameter of each code class.
instance
BGW.Skorokhod.instSeparableSpace
{T : ℝ}
{E : Type u_1}
[MetricSpace E]
[TopologicalSpace.SeparableSpace E]
:
D is separable for J1 when E is (Billingsley 1999, Theorem 12.2; C2).