Finite discretization of uniformly controlled càdlàg paths

Partition lengths are bounded by the minimum spacing. Each partition node is labeled by a finite net in the compact product of the time interval and the state-value set. Equal labels imply small complete Skorokhod distance.

theorem BGW.Skorokhod.totallyBounded_toDComplete_of_partitions {T : ℝ} {E : Type u_1} [MetricSpace E] {A : Set (D T E)} {K : Set E} (hK : IsCompact K) (hA : ∀ f ∈ A, ∀ (t : ↑(Set.Icc 0 T)), f t ∈ K) (hpart : ∀ a > 0, ∃ δ > 0, ∀ f ∈ A, ∃ (n : ℕ) (p : Fin (n + 1) → ℝ), p 0 = 0 ∧ p (Fin.last n) = T ∧ StrictMono p ∧ (∀ (i : Fin n), δ < p i.succ - p i.castSucc) ∧ ∀ (i : Fin n) (s u : ↑(Set.Icc 0 T)), p i.castSucc ≤ ↑s → ↑s < p i.succ → p i.castSucc ≤ ↑u → ↑u < p i.succ → dist (f s) (f u) ≤ a) : TotallyBounded (⇑toDComplete '' A)

A compact value set and uniformly small oscillations on partitions with uniformly positive spacing imply total boundedness in Billingsley's complete metric.