Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-19 06:51 1c60e618

View on Github →

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.

Estimated changes

modified theorem metric.emetric_ball
modified theorem metric.emetric_ball_nnreal