# Definition of integral over level sets in coarea formula

This is probably a simple question, maybe more suited for MSE. In the coarea formula, you have

$$\int_{{\mathbb{R}}^n} g (x) |\nabla f(x)|\, dx= \int_\mathbb{R} \left(\int_{\{f=t\}} g d \mathcal{H}^{n-1} \right)dt ,$$

with $$f$$ Lipshitz and $$g$$ Borel (positive maybe?). Anyway the question is: how do you define the integral $$\int_{\{f=t\}} g d \mathcal{H}^{n-1}$$? When you do the theory of Sobolev spaces it's often remarked that traces of $$L^p$$ functions make no sense, and here you're integrating generic measurable functions basically. I'm sure I (used to) know this but I am not seeing it right now.

If $$f:\mathbb{R}^n\to\mathbb{R}^m$$ is Lipschitz, $$n \geq m$$, and $$A\subseteq \mathbb{R}^n$$ is $$\mathcal{L}^n$$ measurable, then $$A\cap f^{-1}\{y\}$$ is $$\mathcal{H}^{n-m}$$ measurable for $$\mathcal{L}^m$$ almost every $$y$$.
Basically, while for a fixed single level set the trace makes no sense, for almost every level set the trace makes sense. And so you are fine if you are integrating things (or as long as you are working in a context where having $$\int_{\{f =t\}} g d\mathcal{H}^{n-1}$$ defined for almost every $$t$$ is good enough).