This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 7317149

committed

chore(measure_theory/integral): split up measure_theory.integral.lebesgue (#18904)

This PR shortens the 3056-line-long file `measure_theory.integral.lebesgue`, by removing a 1000-line initial segment into a new file `measure_theory.function.simple_func`.

1 parent d20a8cd commit 7317149Copy full SHA for 7317149

4 files changed

src/measure_theory
- function
  - simple_func.lean
  - simple_func_dense.lean
  - strongly_measurable
    - basic.lean
- integral
  - lebesgue.lean

Comments

(0)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Commit 7317149

File tree

0 commit comments