Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-29 21:38 519ab351

View on Github →

feat(topology/metric_space/basic): nonempty intersections of balls (#9448)

Estimated changes

Modified src/data/set/lattice.lean

added theorem set.not_disjoint_iff_nonempty_inter

Modified src/topology/metric_space/basic.lean

added theorem metric.ball_subset_ball'

added theorem metric.closed_ball_subset_closed_ball'

added theorem metric.dist_le_add_of_nonempty_closed_ball_inter_closed_ball

added theorem metric.dist_lt_add_of_nonempty_ball_inter_ball

added theorem metric.dist_lt_add_of_nonempty_ball_inter_closed_ball

added theorem metric.dist_lt_add_of_nonempty_closed_ball_inter_ball