English
For a locally integrable f and a compact set k, there exists an open neighborhood u of k with IntegrableOn f on u.
Русский
Для локально интегрируемой f и компактного k существует открытое соседство u, содержащее k, на котором f интегрируема.
LaTeX
$$$\\exists u,\\ IsOpen(u) \\land k \\subseteq u \\land \\operatorname{IntegrableOn} f u \\mu$$$
Lean4
/-- If a function is locally integrable, then it is integrable on an open neighborhood of any
compact set. -/
theorem integrableOn_nhds_isCompact [PseudoMetrizableSpace ε] (hf : LocallyIntegrable f μ) {k : Set X}
(hk : IsCompact k) : ∃ u, IsOpen u ∧ k ⊆ u ∧ IntegrableOn f u μ :=
by
refine IsCompact.induction_on hk ?_ ?_ ?_ ?_
· refine ⟨∅, isOpen_empty, Subset.rfl, integrableOn_empty⟩
· rintro s t hst ⟨u, u_open, tu, hu⟩
exact ⟨u, u_open, hst.trans tu, hu⟩
· rintro s t ⟨u, u_open, su, hu⟩ ⟨v, v_open, tv, hv⟩
exact ⟨u ∪ v, u_open.union v_open, union_subset_union su tv, hu.union hv⟩
· intro x _
rcases hf x with ⟨u, ux, hu⟩
rcases mem_nhds_iff.1 ux with ⟨v, vu, v_open, xv⟩
exact ⟨v, nhdsWithin_le_nhds (v_open.mem_nhds xv), v, v_open, Subset.rfl, hu.mono_set vu⟩
