Measurable evaluation of extensions from order intervals

A continuous map on an order interval extends to the ambient linearly ordered space by its endpoint values. Evaluation of this extension at a fixed point is measurable for the Borel structure on the space of continuous maps. No compatibility between the order and topology of the domain is needed.

theorem TauCeti.measurable_IccExtend_apply {α : Type u_1} {X : Type u_2} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] {a b : α} (hab : a ≤ b) (t : α) : Measurable fun (γ : C(↑(Set.Icc a b), X)) => Set.IccExtend hab (⇑γ) t

On the space C([a, b], X) of continuous maps, evaluating the map extended by endpoint values outside the order interval [a, b] at a fixed point is measurable.