Skip to content

Commit

Permalink
chore(measure_theory/function/locally_integrable): fix typo (#13160)
Browse files Browse the repository at this point in the history
  • Loading branch information
sgouezel committed Apr 4, 2022
1 parent 6dde651 commit 0cb9407
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/measure_theory/function/locally_integrable.lean
Expand Up @@ -37,7 +37,8 @@ def locally_integrable (f : X → E) (μ : measure X . volume_tac) : Prop :=
lemma integrable.locally_integrable (hf : integrable f μ) : locally_integrable f μ :=
λ K hK, hf.integrable_on

lemma locally_integrable.ae_measurable [sigma_compact_space X] (hf : locally_integrable f μ) :
lemma locally_integrable.ae_strongly_measurable [sigma_compact_space X]
(hf : locally_integrable f μ) :
ae_strongly_measurable f μ :=
begin
rw [← @restrict_univ _ _ μ, ← Union_compact_covering, ae_strongly_measurable_Union_iff],
Expand Down

0 comments on commit 0cb9407

Please sign in to comment.