English
There exists a sequence of open sets whose union covers s and on each the function is integrable on the intersection with s.
Русский
Существует последовательность открытых множеств, чья объединение покрывает s и на каждом множество f интегрируема на пересечении с s.
LaTeX
$$$\\exists (u_n)_{n∈ℕ}, \\forall n, \\text{IsOpen}(u_n) \\land s \\subseteq ⋃_n (u_n) \\land \\text{IntegrableOn}(f, u_n \\cap s)$$$
Lean4
/-- If a function `f` is locally integrable on a set `s` in a second countable topological space,
then there exists a sequence of open sets `u n` covering `s` such that `f` is integrable on each
set `u n ∩ s`. -/
theorem exists_nat_integrableOn [SecondCountableTopology X] (hf : LocallyIntegrableOn f s μ) :
∃ u : ℕ → Set X, (∀ n, IsOpen (u n)) ∧ (s ⊆ ⋃ n, u n) ∧ (∀ n, IntegrableOn f (u n ∩ s) μ) :=
by
rcases hf.exists_countable_integrableOn with ⟨T, T_count, T_open, sT, hT⟩
let T' : Set (Set X) := insert ∅ T
have T'_count : T'.Countable := Countable.insert ∅ T_count
have T'_ne : T'.Nonempty := by simp only [T', insert_nonempty]
rcases T'_count.exists_eq_range T'_ne with ⟨u, hu⟩
refine ⟨u, ?_, ?_, ?_⟩
· intro n
have : u n ∈ T' := by rw [hu]; exact mem_range_self n
rcases mem_insert_iff.1 this with h | h
· rw [h]
exact isOpen_empty
· exact T_open _ h
· intro x hx
obtain ⟨v, hv, h'v⟩ : ∃ v, v ∈ T ∧ x ∈ v := by simpa only [mem_iUnion, exists_prop] using sT hx
have : v ∈ range u := by rw [← hu]; exact subset_insert ∅ T hv
obtain ⟨n, rfl⟩ : ∃ n, u n = v := by simpa only [mem_range] using this
exact mem_iUnion_of_mem _ h'v
· intro n
have : u n ∈ T' := by rw [hu]; exact mem_range_self n
rcases mem_insert_iff.1 this with h | h
· simp only [h, empty_inter, integrableOn_empty]
· exact hT _ h
