Commit 2022-11-01 13:13 6cadbc0d

View on Github →

feat(analysis/normed/group/pointwise): Multiplicativise (#17023) Write the multiplicative version of all lemmas in analysis.normed.group.pointwise and move unrelated lemmas to analysis.normed.group.basic (including deleting a duplicate)

Estimated changes

Modified src/analysis/convex/side.lean

Modified src/analysis/normed/group/basic.lean

added theorem metric.bounded.exists_pos_norm_le'

Modified src/analysis/normed/group/pointwise.lean

deleted theorem add_ball

deleted theorem add_ball_zero

deleted theorem ball_add

deleted theorem ball_add_singleton

deleted theorem ball_add_zero

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

deleted theorem ball_sub

deleted theorem ball_sub_singleton

deleted theorem ball_sub_zero

deleted theorem ball_zero_add_singleton

deleted theorem ball_zero_sub_singleton

deleted theorem bounded_iff_exists_norm_le

deleted theorem closed_ball_add_singleton

added theorem closed_ball_div_singleton

added theorem closed_ball_mul_singleton

added theorem closed_ball_one_div_singleton

added theorem closed_ball_one_mul_singleton

deleted theorem closed_ball_sub_singleton

deleted theorem closed_ball_zero_add_singleton

deleted theorem closed_ball_zero_sub_singleton

added theorem div_ball

added theorem div_ball_one

added theorem inf_edist_inv

added theorem inf_edist_inv_inv

deleted theorem inf_edist_neg

deleted theorem inf_edist_neg_neg

added theorem inv_ball

added theorem inv_closed_ball

added theorem inv_cthickening

added theorem inv_thickening

deleted theorem is_compact.add_closed_ball

deleted theorem is_compact.add_closed_ball_zero

deleted theorem is_compact.closed_ball_add

added theorem is_compact.closed_ball_div

added theorem is_compact.closed_ball_mul

added theorem is_compact.closed_ball_one_div

added theorem is_compact.closed_ball_one_mul

deleted theorem is_compact.closed_ball_sub

deleted theorem is_compact.closed_ball_zero_add

deleted theorem is_compact.closed_ball_zero_sub

added theorem is_compact.div_closed_ball

added theorem is_compact.div_closed_ball_one

added theorem is_compact.mul_closed_ball

added theorem is_compact.mul_closed_ball_one

deleted theorem is_compact.sub_closed_ball

deleted theorem is_compact.sub_closed_ball_zero

deleted theorem metric.bounded.add

added theorem metric.bounded.div

deleted theorem metric.bounded.exists_pos_norm_le

added theorem metric.bounded.inv

added theorem metric.bounded.mul

deleted theorem metric.bounded.neg

deleted theorem metric.bounded.sub

added theorem mul_ball

added theorem mul_ball_one

deleted theorem neg_ball

deleted theorem neg_closed_ball

deleted theorem neg_cthickening

deleted theorem neg_thickening

deleted theorem singleton_add_ball

deleted theorem singleton_add_ball_zero

deleted theorem singleton_add_closed_ball

deleted theorem singleton_add_closed_ball_zero

added theorem singleton_div_ball

added theorem singleton_div_ball_one

added theorem singleton_div_closed_ball

added theorem singleton_div_closed_ball_one

added theorem singleton_mul_ball

added theorem singleton_mul_ball_one

added theorem singleton_mul_closed_ball

added theorem singleton_mul_closed_ball_one

deleted theorem singleton_sub_ball

deleted theorem singleton_sub_ball_zero

deleted theorem singleton_sub_closed_ball

deleted theorem singleton_sub_closed_ball_zero

added theorem smul_ball_one

added theorem smul_closed_ball_one

deleted theorem sub_ball

deleted theorem sub_ball_zero

deleted theorem vadd_ball_zero

deleted theorem vadd_closed_ball_zero

Modified src/analysis/normed_space/pointwise.lean

Modified src/analysis/normed_space/spectrum.lean