mathlib
0eb49606 - chore(topology/noetherian_space): golf (#18394)

Commit

3 years ago

chore(topology/noetherian_space): golf (#18394) Also generalize `noetherian_space.set` to `inducing.noetherian_space`.

References

Author

urkud

Parents