English
There exists a countable collection of open sets with the stated integrability properties for a locally integrable function.
Русский
Существуют счетные открытые множества, на которых выполняются условия интегрируемости для локально интегрируемой функции.
LaTeX
$$$\\exists T: Set(Set X), T\\text{ счетно}, \\text{(conditions)}$$$
Lean4
/-- If a function `f` is locally integrable on a set `s` in a second countable topological space,
then there exist countably many open sets `u` covering `s` such that `f` is integrable on each
set `u ∩ s`. -/
theorem exists_countable_integrableOn [SecondCountableTopology X] (hf : LocallyIntegrableOn f s μ) :
∃ T : Set (Set X), T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ (s ⊆ ⋃ u ∈ T, u) ∧ (∀ u ∈ T, IntegrableOn f (u ∩ s) μ) :=
by
have : ∀ x : s, ∃ u, IsOpen u ∧ x.1 ∈ u ∧ IntegrableOn f (u ∩ s) μ :=
by
rintro ⟨x, hx⟩
rcases hf x hx with ⟨t, ht, h't⟩
rcases mem_nhdsWithin.1 ht with ⟨u, u_open, x_mem, u_sub⟩
exact ⟨u, u_open, x_mem, h't.mono_set u_sub⟩
choose u u_open xu hu using this
obtain ⟨T, T_count, hT⟩ : ∃ T : Set s, T.Countable ∧ s ⊆ ⋃ i ∈ T, u i :=
by
have : s ⊆ ⋃ x : s, u x := fun y hy => mem_iUnion_of_mem ⟨y, hy⟩ (xu ⟨y, hy⟩)
obtain ⟨T, hT_count, hT_un⟩ := isOpen_iUnion_countable u u_open
exact ⟨T, hT_count, by rwa [hT_un]⟩
refine ⟨u '' T, T_count.image _, ?_, by rwa [biUnion_image], ?_⟩
· rintro v ⟨w, -, rfl⟩
exact u_open _
· rintro v ⟨w, -, rfl⟩
exact hu _
