Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-30 09:54 30649f55

View on Github →

cleanup instances/ennreal

Estimated changes

Modified src/topology/instances/ennreal.lean

added theorem continuous_edist'

added theorem continuous_edist

added theorem continuous_of_le_add_edist

added theorem edist_ne_top_of_mem_ball

added theorem emetric.cauchy_seq_iff_le_tendsto_0

deleted theorem emetric.continuous_edist

deleted theorem emetric.edist_ne_top_of_mem_ball

deleted def emetric.metric_space_emetric_ball

deleted theorem emetric.nhds_eq_nhds_emetric_ball

added def metric_space_emetric_ball

added theorem nhds_eq_nhds_emetric_ball

added theorem tendsto_edist