Continuity partitions for Skorokhod representation

A separable metric space admits countable Borel partitions of arbitrarily small mesh whose cells have null frontier for a prescribed finite measure. These are the spatial partitions in Billingsley's proof of the representation theorem.

theorem BGW.Probability.exists_continuity_partition {S : Type u_1} [PseudoMetricSpace S] [TopologicalSpace.SeparableSpace S] [Nonempty S] [MeasurableSpace S] [OpensMeasurableSpace S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure μ] {ε : ℝ} (hε : 0 < ε) : ∃ (A : ℕ → Set S), (∀ (j : ℕ), MeasurableSet (A j)) ∧ Pairwise (Function.onFun Disjoint A) ∧ ⋃ (j : ℕ), A j = Set.univ ∧ (∀ (j : ℕ), μ (frontier (A j)) = 0) ∧ ∀ (j : ℕ), ∀ x ∈ A j, ∀ y ∈ A j, dist x y < ε

A finite Borel measure on a nonempty separable metric space admits a countable Borel partition of arbitrarily small mesh, all of whose cells have null frontier. Empty cells are permitted; the covering and disjointness statements are exact, rather than almost everywhere.