Skip to content

Commit

Permalink
chore(measure_theory/set_integral): use weaker assumptions here and t…
Browse files Browse the repository at this point in the history 
…here (#5647)

* use `ae_measurable f (μ.restrict s)` in more lemmas;
* introduce `measurable_at_filter` and use it.
  • Loading branch information
@urkud
urkud committed Jan 10, 2021
1 parent 3e7efd4 commit 62c1912
Show file tree
Hide file tree
Showing 4 changed files with 317 additions and 158 deletions.

0 comments on commit 62c1912

Please sign in to comment.