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
andmetric_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