# Measurability of the line derivative #

We prove in `measurable_lineDeriv`

that the line derivative of a function (with respect to a
locally compact scalar field) is measurable, provided the function is continuous.

In `measurable_lineDeriv_uncurry`

, assuming additionally that the source space is second countable,
we show that `(x, v) ↦ lineDeriv 𝕜 f x v`

is also measurable.

An assumption such as continuity is necessary, as otherwise one could alternate in a non-measurable
way between differentiable and non-differentiable functions along the various lines
directed by `v`

.

Measurability of the line derivative `lineDeriv 𝕜 f x v`

with respect to a fixed direction `v`

.

Measurability of the line derivative `lineDeriv 𝕜 f x v`

when varying both `x`

and `v`

. For this,
we need an additional second countability assumption on `E`

to make sure that open sets are
measurable in `E × E`

.