Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-02 13:55 a88356ff

View on Github →

chore(topology/metric_space): use dot notation (#2313)

  • in continuous.dist and continuous.edist;
  • in tendsto.dist and tendsto.edist.

Estimated changes

added theorem continuous.edist
deleted theorem continuous_edist'
modified theorem continuous_edist
added theorem filter.tendsto.edist
deleted theorem tendsto_edist
added theorem continuous.dist
added theorem continuous.nndist
deleted theorem continuous_dist'
modified theorem continuous_dist
deleted theorem continuous_nndist'
modified theorem continuous_nndist
added theorem filter.tendsto.dist
added theorem filter.tendsto.nndist
deleted theorem tendsto_dist
deleted theorem tendsto_nndist'