locallyIntegrableOn_univ — Mathlib

English

For any f, locally integrable on the whole space with respect to μ is equivalent to locally integrable on univ with respect to μ.

Русский

Для любого f локально интегрируемого по μ на всём пространстве эквивалентно локально интегрируемому на всю вселенную (univ) по μ.

LaTeX

$$$\\operatorname{LocallyIntegrableOn}(f,\\mathrm{univ},\\mu) \\iff \\operatorname{LocallyIntegrable}(f,\\mu)$$$

Lean4

theorem locallyIntegrableOn_univ : LocallyIntegrableOn f univ μ ↔ LocallyIntegrable f μ := by
  simp only [LocallyIntegrableOn, nhdsWithin_univ, mem_univ, true_imp_iff]; rfl

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