Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-28 19:34 e62c534c

View on Github →

add ennreal.to_real

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.of_real_add

added theorem ennreal.of_real_eq_zero

added theorem ennreal.of_real_le_of_real

added theorem ennreal.of_real_le_of_real_iff

added theorem ennreal.of_real_lt_of_real_iff

added theorem ennreal.of_real_ne_top

added theorem ennreal.of_real_one

added theorem ennreal.of_real_pos

added theorem ennreal.of_real_to_real

added theorem ennreal.of_real_zero

added theorem ennreal.to_real_add

added theorem ennreal.to_real_eq_zero_iff

added theorem ennreal.to_real_le_to_real

added theorem ennreal.to_real_lt_to_real

added theorem ennreal.to_real_nonneg

added theorem ennreal.to_real_of_real

added theorem ennreal.top_ne_of_real

added theorem ennreal.top_to_real

added theorem ennreal.zero_to_real

Modified src/data/real/nnreal.lean

added theorem nnreal.of_real_one

Modified src/topology/instances/ennreal.lean

added theorem ennreal.continuous_of_real

added theorem ennreal.tendsto_of_real

Modified src/topology/metric_space/basic.lean

added theorem dist_edist

deleted theorem dist_eq_edist

deleted theorem dist_eq_nndist

added theorem dist_nndist

modified theorem edist_dist

deleted theorem edist_eq_dist

deleted theorem edist_eq_nndist

added theorem edist_nndist

added def emetric_space.to_metric_space

added theorem metric.emetric_ball

added theorem metric.emetric_closed_ball

added theorem nndist_dist

added theorem nndist_edist

deleted theorem nndist_eq_dist

deleted theorem nndist_eq_edist

added theorem sum.dist_eq

Modified src/topology/metric_space/emetric_space.lean

added theorem emetric.ball_eq_empty_iff

added theorem emetric.mem_closed_ball_self