locallyIntegrableOn_const — Mathlib

English

If a constant-valued function is locally integrable, then its constant value is locally integrable (provided measure is locally finite).

Русский

Если функция с константными значениями локально интегрируема, то и сама константа интегрируема локально (при локально конечной мере).

LaTeX

$$$\\operatorname{LocallyIntegrable} \\big( x \\mapsto c \\big) \\mu \\iff \\text{(condition)}$$$

Lean4

theorem locallyIntegrableOn_const [IsLocallyFiniteMeasure μ] (c : E) : LocallyIntegrableOn (fun _ => c) s μ :=
  locallyIntegrableOn_const_enorm enorm_ne_top

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