mathlib3
97c9ef8c - chore(measure_theory): use notation `measurable_set[m]` (#14690)

Commit

3 years ago

chore(measure_theory): use notation `measurable_set[m]` (#14690)

Author

urkud

urkud

Parents

Loading