Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-10 16:32 93ba8b6d

View on Github →

refactor(topology/metric_space): introduce&use edist/dist bases (#1969)

  • refactor(topology/metric_space): introduce&use edist/dist bases
  • Introduce bases for emetric_space and metric_space.
  • Make some proofs use general facts about filter bases.
  • Fix some lint errors
  • Update src/topology/metric_space/emetric_space.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
  • +2 docstrings

Estimated changes