Measurable reconstruction from a dense trace

A continuous real function is reconstructed Borel-measurably from its values on a countable dense subset, with the zero function on the branch where no continuous reconstruction exists.

theorem BGW.Probability.measurable_continuous_reconstruction {X : Type u_1} {Ω : Type u_2} [TopologicalSpace X] [MeasurableSpace Ω] [PolishSpace C(X, ℝ)] (D : Set X) [Countable ↑D] (hD : Dense D) (a : Ω → ↑D → ℝ) (ha : Measurable a) : Measurable fun (ω : Ω) => if h : ∃ (g : C(X, ℝ)), ∀ (t : ↑D), g ↑t = a ω t then Classical.choose h else 0

Reconstruction of a continuous function from a countable dense trace is Borel.