Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-06 12:13 767e6ae0

View on Github →

refactor(topology): make two definitions irreducible from the start (#6060)

Estimated changes

Modified src/topology/basic.lean

modified def nhds

modified theorem nhds_def

Modified src/topology/metric_space/hausdorff_distance.lean

modified def emetric.Hausdorff_edist