mathlib
11bb0c91 - feat(measure_theory/integral/layercake): Add versions of layercake formula with strict inequality. (#17920)

Commit
3 years ago
feat(measure_theory/integral/layercake): Add versions of layercake formula with strict inequality. (#17920) This PR adds versions of layercake formula with measures of sets strictly above a given level, i.e., of the form `{x | f x > t}`. This is useful particularly when `f` is continuous and one wants the set in question to be open (rather than closed). Co-authored-by: Kalle-swift <kalle.kytola@aalto.fi> Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
Author
kkytola
Parents
Loading