Uniform limits of càdlàg paths

Completeness of the state space supplies the left limits of a uniform limit. No completeness claim for the ordinary J1 metric is used.

theorem BGW.Skorokhod.isCadlag_of_tendstoUniformly {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [Preorder X] [MetricSpace E] [CompleteSpace E] {F : ℕ → X → E} {f : X → E} (hF : ∀ (n : ℕ), IsCadlag (F n)) (h : TendstoUniformly F f Filter.atTop) : IsCadlag f

Uniform limits of càdlàg functions into a complete metric space are càdlàg.

theorem BGW.Skorokhod.exists_cadlag_uniform_limit {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [Preorder X] [MetricSpace E] [CompleteSpace E] (F : ℕ → X → E) (hF : ∀ (n : ℕ), IsCadlag (F n)) (hC : UniformCauchySeqOn F Filter.atTop Set.univ) : ∃ (f : X → E), IsCadlag f ∧ TendstoUniformly F f Filter.atTop

A uniformly Cauchy sequence of càdlàg functions has a càdlàg uniform limit.