mathlib3
3ce4161c - refactor(measure_theory/integral): restrict interval integrals to real intervals (#12754)

Commit

3 years ago

refactor(measure_theory/integral): restrict interval integrals to real intervals (#12754) This way `∫ x in 0 .. 1, (1 : real)` means what it should, not `∫ x : nat in 0 .. 1, (1 : real)`.

Author

urkud

Parents

b0f585c5

mathlib3 3ce4161c - refactor(measure_theory/integral): restrict interval integrals to real intervals (#12754)

mathlib3
3ce4161c - refactor(measure_theory/integral): restrict interval integrals to real intervals (#12754)