mathlib3
b9cb69c3 - feat(topology/order): make nhds irreducible (#1043)

Commit

6 years ago

feat(topology/order): make nhds irreducible (#1043) * feat(topology/order): make nhds irreducible * move nhds irreducible to topology.basic

References

Author

robertylewis

Committer

mergify[bot]

Parents