mathlib3
d39590fc - refactor(topology/sets/opens): use a `structure` for `opens` and `open_nhds_of` (#18409)

Commit
2 years ago
refactor(topology/sets/opens): use a `structure` for `opens` and `open_nhds_of` (#18409) Also review API.
Author
Parents
Loading