Mathlib v3 is deprecated. Go to Mathlib v4

Theorem metric.emetric_closed_ball_nnreal

Modification history

2021-08-19 06:51
src/topology/metric_space/basic.lean
feat(topology/metric_space/basic): `emetric.ball x ∞ = univ` (#8745) …
Modified metric.emetric_closed_ball_nnrealView on Github →
2020-12-16 07:31
src/topology/metric_space/basic.lean
chore(*): use notation `ℝ≥0` (#5391)
Modified metric.emetric_closed_ball_nnrealView on Github →
2020-04-06 15:34
src/topology/metric_space/basic.lean
feat(topology/bounded_continuous_function): composition of limits when uniform convergence (#2260) …
Added metric.emetric_closed_ball_nnrealView on Github →