English
For a measurable set s, the function f restricted to s is locally integrable with respect to μ.comap Subtype.val if and only if f is locally integrable on s with respect to μ.
Русский
Пусть s – измеримое множество. Функция f, ограниченная на s, локально интегрируема по отношению к μ.comap Subtype.val тогда и только тогда, когда f локально интегрируема на s по μ.
LaTeX
$$$\\operatorname{LocallyIntegrable}\\big( f\\!,\,s\\big)\\, (\\mu\\circ \\mathrm{Subtype.val}^{-1}) \\ \\iff\\ \\operatorname{LocallyIntegrableOn} f\\ s\\ \\mu$$$
Lean4
theorem locallyIntegrable_comap (hs : MeasurableSet s) :
LocallyIntegrable (fun x : s ↦ f x) (μ.comap Subtype.val) ↔ LocallyIntegrableOn f s μ :=
by
simp_rw [LocallyIntegrableOn, Subtype.forall', ← map_nhds_subtype_val]
exact forall_congr' fun _ ↦ (MeasurableEmbedding.subtype_coe hs).integrableAtFilter_iff_comap.symm
