integrableAt_nhds — Mathlib

English

If f is continuous on t, and a is any point, then f is integrable at nhds a with respect to μ.

Русский

Если f непрерывна на t, то f интегрируема в nhds a по μ.

LaTeX

$$$\\text{IntegrableAtFilter } f (\\nhds a) μ$ under suitable hypotheses.$$

Lean4

theorem integrableAt_nhds [TopologicalSpace α] [SecondCountableTopologyEither α E] [OpensMeasurableSpace α]
    {μ : Measure α} [IsLocallyFiniteMeasure μ] {f : α → E} (hf : Continuous f) (a : α) : IntegrableAtFilter f (𝓝 a) μ :=
  by
  rw [← nhdsWithin_univ]
  exact hf.continuousOn.integrableAt_nhdsWithin MeasurableSet.univ (mem_univ a)

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