Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-28 17:14 8572c6b0

View on Github →

feat(topology): prove continuity of nndist and edist; ball a r is a metric space

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem continuous_nnnorm

added theorem continuous_smul

Modified src/data/real/ennreal.lean

added theorem ennreal.infi_ennreal

added theorem ennreal.mul_lt_top

Modified src/topology/instances/ennreal.lean

added theorem emetric.continuous_edist

added theorem emetric.edist_ne_top_of_mem_ball

added def emetric.metric_space_emetric_ball

added theorem emetric.nhds_eq_nhds_emetric_ball

added theorem infi_real_pos_eq_infi_nnreal_pos

Modified src/topology/instances/nnreal.lean

Modified src/topology/metric_space/basic.lean

added theorem continuous_nndist'

added theorem tendsto_nndist'

added theorem uniform_continuous_nndist'

Modified src/topology/metric_space/emetric_space.lean

added theorem uniformity_edist_nnreal