Small-oscillation partitions of càdlàg paths

The existence argument uses the supremum of the times reachable by a finite partition. Left limits make that supremum reachable, and right continuity extends it.

theorem BGW.Skorokhod.exists_partition_dist_le {T : ℝ} {E : Type u_1} [MetricSpace E] (f : D T E) (hT : 0 ≤ T) {ε : ℝ} (hε : 0 < ε) : ∃ (r : ℕ) (t : Fin (r + 1) → ℝ), t 0 = 0 ∧ t (Fin.last r) = T ∧ StrictMono t ∧ ∀ (i : Fin r) (s u : ↑(Set.Icc 0 T)), t i.castSucc ≤ ↑s → ↑s < t i.succ → t i.castSucc ≤ ↑u → ↑u < t i.succ → dist (f s) (f u) ≤ ε

A càdlàg path admits a finite partition with arbitrarily small oscillation on each half-open block. The terminal value is deliberately excluded from the last block.