locallyIntegrableOn — Mathlib

English

A continuous function is locally integrable with respect to any locally finite measure.

Русский

Непрерывная функция локально интегрируема по любой локально конечной мере.

LaTeX

$$$\text{IsLocallyFiniteMeasure}(\mu) \Rightarrow \operatorname{LocallyIntegrable}(f, \mu)$$$

Lean4

/-- A function `f` continuous on a set `K` is locally integrable on this set with respect
to any locally finite measure. -/
theorem locallyIntegrableOn [IsLocallyFiniteMeasure μ] [SecondCountableTopologyEither X E] (hf : ContinuousOn f K)
    (hK : MeasurableSet K) : LocallyIntegrableOn f K μ := fun _x hx => hf.integrableAt_nhdsWithin hK hx

Похожие утверждения