Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-19 12:47 b9cb69c3

View on Github →

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

  • feat(topology/order): make nhds irreducible
  • move nhds irreducible to topology.basic

Estimated changes

added theorem le_nhds_iff
added theorem nhds_def
added theorem nhds_le_of_le