exists_nat_integrableOn — Mathlib

English

If f is locally integrable, then it is locally integrable on any s.

Русский

Если f локально интегрируема, то она локально интегрируема на любом подмножестве s.

LaTeX

$$$\\operatorname{LocallyIntegrable} f \\mu \\Rightarrow \\forall s,\\operatorname{LocallyIntegrableOn} f s \\mu$$$

Lean4

/-- If a function is locally integrable in a second countable topological space,
then there exists a sequence of open sets covering the space on which it is integrable. -/
theorem exists_nat_integrableOn [SecondCountableTopology X] (hf : LocallyIntegrable f μ) :
    ∃ u : ℕ → Set X, (∀ n, IsOpen (u n)) ∧ ((⋃ n, u n) = univ) ∧ (∀ n, IntegrableOn f (u n) μ) :=
  by
  rcases (hf.locallyIntegrableOn univ).exists_nat_integrableOn with ⟨u, u_open, u_union, hu⟩
  refine ⟨u, u_open, eq_univ_of_univ_subset u_union, fun n ↦ ?_⟩
  simpa only [inter_univ] using hu n

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