Mathlib v3 is deprecated. Go to Mathlib v4

Theorem metric.emetric_ball_top

Modification history

2021-08-19 06:51

src/topology/metric_space/basic.lean

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

Added metric.emetric_ball_top View on Github →