This repository was archived by the owner on Jul 24, 2024. It is now read-only.
Commit 08a4542
committed
feat(measure_theory/function): Functions locally integrable on a set (#18673)
This PR adds a definition for local integrability of a function on a set (a relative version of the existing "locally integrable"), and proves some elementary properties of this definition (in particular, functions continuous on `s` are locally integrable on `s`).1 parent e655e4e commit 08a4542
5 files changed
Lines changed: 285 additions & 101 deletions
File tree
- src/measure_theory
- function
- integral
0 commit comments