Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-29 20:31 812e17f8

View on Github →

feat(analysis/normed_space/pointwise): Addition of balls (#13381) Adding two balls yields another ball.

Estimated changes

added theorem dist_neg
modified theorem dist_neg_neg
added theorem edist_neg
modified theorem edist_neg_neg
added theorem add_ball
added theorem add_ball_zero
added theorem ball_add
modified theorem ball_add_singleton
added theorem ball_add_zero
added theorem ball_sub
added theorem ball_sub_singleton
added theorem ball_sub_zero
modified theorem ball_zero_add_singleton
modified theorem bounded_iff_exists_norm_le
modified theorem closed_ball_add_singleton
added theorem inf_edist_neg
added theorem inf_edist_neg_neg
modified theorem metric.bounded.add
added theorem metric.bounded.neg
added theorem metric.bounded.sub
added theorem neg_ball
added theorem neg_closed_ball
added theorem neg_cthickening
added theorem neg_thickening
modified theorem singleton_add_ball
modified theorem singleton_add_ball_zero
modified theorem singleton_add_closed_ball
added theorem singleton_sub_ball
added theorem sub_ball
added theorem sub_ball_zero
added theorem vadd_ball_zero
added theorem vadd_closed_ball_zero
added theorem ball_add_ball
added theorem ball_add_closed_ball
added theorem ball_sub_ball
added theorem ball_sub_closed_ball
added theorem closed_ball_add_ball
added theorem closed_ball_sub_ball
added theorem cthickening_ball
added theorem thickening_ball
added theorem thickening_closed_ball
deleted theorem vadd_ball_zero
deleted theorem vadd_closed_ball_zero
modified theorem set.inv_singleton