Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-05 15:43 2f07ff21

View on Github →

chore(topology/metric_space): more norm_cast lemmas, golf proofs (#4911)

Estimated changes

Modified src/data/real/nnreal.lean

Modified src/topology/metric_space/basic.lean

added theorem coe_nndist

added theorem dist_le_coe

added theorem dist_le_pi_dist

added theorem dist_lt_coe

added theorem edist_le_coe

added theorem edist_lt_coe

added theorem ennreal_coe_nndist

added theorem nndist_le_pi_nndist

added theorem nndist_pi_def

Modified src/topology/metric_space/emetric_space.lean

added theorem edist_pi_def