mathlib
02d02dfc - chore(measure_theory): fix TC assumptions in 2 lemmas (#11185)

Commit

4 years ago

chore(measure_theory): fix TC assumptions in 2 lemmas (#11185) With new assumptions, these lemmas work, e.g., for `β = ι → ℝ`.

Author

urkud

Parents