Commit 2023-04-07 19:59 d9a1c78b

View on Github →

feat: port Analysis.Normed.Group.Pointwise (#3331)

Estimated changes

added theorem Metric.Bounded.div
added theorem Metric.Bounded.inv
added theorem Metric.Bounded.mul
added theorem ball_div
added theorem ball_div_one
added theorem ball_div_singleton
added theorem ball_mul
added theorem ball_mul_one
added theorem ball_mul_singleton
added theorem ball_one_div_singleton
added theorem ball_one_mul_singleton
added theorem div_ball
added theorem div_ball_one
added theorem infEdist_inv
added theorem infEdist_inv_inv
added theorem inv_ball
added theorem inv_closedBall
added theorem inv_cthickening
added theorem inv_thickening
added theorem mul_ball
added theorem mul_ball_one
added theorem singleton_div_ball
added theorem singleton_div_ball_one
added theorem singleton_mul_ball
added theorem singleton_mul_ball_one
added theorem smul_ball_one
added theorem smul_closedBall_one