Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-27 20:26 0a9a1ff4

View on Github →

refactor(topology/algebra/ordered): use tfae, prove equality of some nhds_within (#1831)

  • refactor(topology/algebra/ordered): use tfae, prove equality of some nhds_within
  • Add missing order_dual.* instances
  • Try to fix the build
  • Fix formatting, rename some variables
  • Fix compile

Estimated changes