Measurability detected by distances #
A map into a second-countable metric Borel space is measurable when all of its distance functions to fixed target points are measurable.
An extended-distance variant of measurable_of_dist_functions for metric spaces.
theorem
LiebThirring.measurable_of_dist_functions
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[MetricSpace E]
[SecondCountableTopology E]
[MeasurableSpace E]
[BorelSpace E]
(f : α → E)
(hf : ∀ (h : E), Measurable fun (x : α) => dist (f x) h)
:
A map into a second-countable metric Borel space is measurable when all of its distance functions to fixed target points are measurable.