locallyIntegrableOn_const_enorm — Mathlib

English

Locally integrable on a closed set is equivalent to locally integrable with restricted measure on that set (repeat).

Русский

Локальная интегрируемость на замыкании эквивалентна локальной интегрируемости при ограниченной мере на этом множестве (повтор).

LaTeX

$$$\\text{IsClosed } s \\Rightarrow (\\operatorname{LocallyIntegrableOn} f s \\mu \\iff \\operatorname{LocallyIntegrable} f (\\mu.restrict s))$$$

Lean4

theorem locallyIntegrableOn_const_enorm [IsLocallyFiniteMeasure μ] {c : ε} (hc : ‖c‖ₑ ≠ ∞) :
    LocallyIntegrableOn (fun _ => c) s μ :=
  (locallyIntegrable_const_enorm hc).locallyIntegrableOn s

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