mathlib

1c60e618 - feat(topology/metric_space/basic): `emetric.ball x ∞ = univ` (#8745)

feat(topology/metric_space/basic): `emetric.ball x ∞ = univ` (#8745) * add `@[simp]` to `metric.emetric_ball`, `metric.emetric_ball_nnreal`, and `metric.emetric_closed_ball_nnreal`; * add `@[simp]` lemmas `metric.emetric_ball_top` and `emetric.closed_ball_top`.