mathlib3
b0de8114 - chore(measure_theory/borel_space): DRY by using `order_dual` (#3685)

Commit

5 years ago

chore(measure_theory/borel_space): DRY by using `order_dual` (#3685)

Author

urkud

urkud

Parents

Loading