Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-06 17:50 5b0dd140

View on Github →

feat(analysis/normed/group/basic): Multiplicative, noncommutative normed groups (#15705) Define

  • seminormed_group
  • seminormed_add_group
  • seminormed_comm_group
  • normed_group
  • normed_add_group
  • normed_comm_group Multiplicativize all lemmas in analysis.normed.group.basic. To disambiguate names, I add one or two ' to the multiplicative version where needed.

Estimated changes

added theorem le_map_div_add_map_div
added theorem abs_norm_sub_norm_le'
deleted theorem abs_norm_sub_norm_le
deleted theorem add_mem_ball_iff_norm
deleted theorem add_subgroup.coe_norm
deleted theorem add_subgroup.norm_coe
added theorem ball_eq'
deleted theorem ball_eq
added theorem ball_one_eq
deleted theorem ball_zero_eq
added theorem coe_comp_nnnorm'
deleted theorem coe_comp_nnnorm
added theorem coe_nnnorm'
deleted theorem coe_nnnorm
deleted theorem coe_norm_add_group_norm
added theorem coe_norm_group_norm
added theorem comap_norm_nhds_one
deleted theorem comap_norm_nhds_zero
added theorem continuous.nnnorm'
deleted theorem continuous.nnnorm
added theorem continuous.norm'
deleted theorem continuous.norm
added theorem continuous_at.nnnorm'
deleted theorem continuous_at.nnnorm
added theorem continuous_at.norm'
deleted theorem continuous_at.norm
added theorem continuous_nnnorm'
deleted theorem continuous_nnnorm
added theorem continuous_norm'
deleted theorem continuous_norm
added theorem continuous_on.nnnorm'
deleted theorem continuous_on.nnnorm
added theorem continuous_on.norm'
deleted theorem continuous_on.norm
deleted theorem continuous_within_at.norm
deleted theorem dist_add_add_le
deleted theorem dist_add_add_le_of_le
deleted theorem dist_add_left
deleted theorem dist_add_right
added theorem dist_div_div_le
added theorem dist_div_div_le_of_le
added theorem dist_div_left
added theorem dist_div_right
deleted theorem dist_eq_norm'
deleted theorem dist_eq_norm
added theorem dist_eq_norm_div'
added theorem dist_eq_norm_div
added theorem dist_inv
added theorem dist_inv_inv
deleted theorem dist_le_norm_add_norm
added theorem dist_le_norm_mul_norm
added theorem dist_mul_left
added theorem dist_mul_mul_le
added theorem dist_mul_mul_le_of_le
added theorem dist_mul_right
deleted theorem dist_neg
deleted theorem dist_neg_neg
added theorem dist_norm_norm_le'
deleted theorem dist_norm_norm_le
added theorem dist_one_left
added theorem dist_one_right
added theorem dist_prod_prod_le
deleted theorem dist_self_add_left
deleted theorem dist_self_add_right
added theorem dist_self_div_left
added theorem dist_self_div_right
added theorem dist_self_mul_left
added theorem dist_self_mul_right
deleted theorem dist_self_sub_left
deleted theorem dist_self_sub_right
deleted theorem dist_sub_left
deleted theorem dist_sub_right
deleted theorem dist_sub_sub_le
deleted theorem dist_sub_sub_le_of_le
deleted theorem dist_sum_sum_le
deleted theorem dist_sum_sum_le_of_le
deleted theorem dist_zero_left
deleted theorem dist_zero_right
deleted theorem edist_add_add_le
deleted theorem edist_add_left
deleted theorem edist_add_right
added theorem edist_div_left
added theorem edist_div_right
added theorem edist_eq_coe_nnnorm'
deleted theorem edist_eq_coe_nnnorm
deleted theorem edist_eq_coe_nnnorm_sub
added theorem edist_inv
added theorem edist_inv_inv
added theorem edist_mul_left
added theorem edist_mul_mul_le
added theorem edist_mul_right
deleted theorem edist_neg
deleted theorem edist_neg_neg
deleted theorem edist_sub_left
deleted theorem edist_sub_right
added theorem eq_of_norm_div_le_zero
deleted theorem eq_of_norm_sub_eq_zero
deleted theorem eq_of_norm_sub_le_zero
added theorem filter.tendsto.nnnorm'
deleted theorem filter.tendsto.nnnorm
added theorem filter.tendsto.norm'
deleted theorem filter.tendsto.norm
deleted theorem isometric.add_left_symm
deleted theorem isometric.add_right_apply
deleted theorem isometric.add_right_symm
deleted theorem isometric.coe_add_left
deleted theorem isometric.coe_add_right
added theorem isometric.coe_inv
added theorem isometric.coe_mul_left
deleted theorem isometric.coe_neg
added theorem isometric.inv_symm
added theorem isometric.inv_to_equiv
deleted theorem isometric.neg_symm
deleted theorem isometric.neg_to_equiv
deleted theorem lipschitz_with.add
added theorem lipschitz_with.div
added theorem lipschitz_with.inv
added theorem lipschitz_with.mul'
deleted theorem lipschitz_with.neg
deleted theorem lipschitz_with.sub
deleted theorem lipschitz_with_one_nnnorm
deleted theorem lipschitz_with_one_norm
added theorem mem_ball_iff_norm'''
added theorem mem_ball_iff_norm''
deleted theorem mem_ball_iff_norm'
deleted theorem mem_ball_iff_norm
added theorem mem_ball_one_iff
deleted theorem mem_ball_zero_iff
deleted theorem mem_closed_ball_iff_norm'
deleted theorem mem_closed_ball_iff_norm
deleted theorem mem_closed_ball_zero_iff
deleted theorem mem_emetric_ball_zero_iff
added theorem mem_sphere_iff_norm'
deleted theorem mem_sphere_iff_norm
deleted theorem mem_sphere_zero_iff_norm
added theorem mul_mem_ball_iff_norm
added theorem ne_one_of_mem_sphere
added theorem ne_one_of_norm_ne_zero
deleted theorem ne_zero_of_mem_sphere
deleted theorem ne_zero_of_nnnorm_ne_zero
deleted theorem ne_zero_of_norm_ne_zero
deleted theorem nndist_add_add_le
deleted theorem nndist_eq_nnnorm
added theorem nndist_eq_nnnorm_div
added theorem nndist_mul_mul_le
deleted theorem nndist_nnnorm_nnnorm_le
deleted theorem nnnorm_add_le
added theorem nnnorm_div_le
added theorem nnnorm_eq_zero'
deleted theorem nnnorm_eq_zero
added theorem nnnorm_inv'
deleted theorem nnnorm_le_add_nnnorm_add
deleted theorem nnnorm_le_insert'
deleted theorem nnnorm_le_insert
added theorem nnnorm_le_pi_nnnorm'
deleted theorem nnnorm_le_pi_nnnorm
added theorem nnnorm_mul_le'
deleted theorem nnnorm_multiset_sum_le
added theorem nnnorm_ne_zero_iff'
deleted theorem nnnorm_ne_zero_iff
deleted theorem nnnorm_neg
added theorem nnnorm_of_add
added theorem nnnorm_of_dual
added theorem nnnorm_of_mul
added theorem nnnorm_one'
added theorem nnnorm_prod_le
added theorem nnnorm_prod_le_of_le
deleted theorem nnnorm_sub_le
deleted theorem nnnorm_sum_le
deleted theorem nnnorm_sum_le_of_le
added theorem nnnorm_to_add
added theorem nnnorm_to_dual
added theorem nnnorm_to_mul
deleted theorem nnnorm_zero
deleted def norm_add_group_norm
deleted theorem norm_add_le
deleted theorem norm_add_le_of_le
deleted theorem norm_add₃_le
added theorem norm_div_eq_zero_iff
added theorem norm_div_le
added theorem norm_div_le_of_le
added theorem norm_div_pos_iff
added theorem norm_div_rev
added theorem norm_eq_of_mem_sphere'
deleted theorem norm_eq_of_mem_sphere
added theorem norm_eq_zero'''
added theorem norm_eq_zero''
deleted theorem norm_eq_zero
deleted theorem norm_eq_zero_iff'
modified theorem norm_fst_le
added def norm_group_norm
added theorem norm_inv'
deleted theorem norm_le_add_norm_add
deleted theorem norm_le_insert'
deleted theorem norm_le_insert
added theorem norm_le_mul_norm_add
added theorem norm_le_pi_norm'
deleted theorem norm_le_pi_norm
added theorem norm_le_zero_iff'''
added theorem norm_le_zero_iff''
deleted theorem norm_le_zero_iff'
deleted theorem norm_le_zero_iff
added theorem norm_lt_of_mem_ball'
deleted theorem norm_lt_of_mem_ball
added theorem norm_mul_le'
added theorem norm_mul_le_of_le
added theorem norm_multiset_prod_le
modified theorem norm_multiset_sum_le
added theorem norm_mul₃_le
added theorem norm_ne_zero_iff'
deleted theorem norm_ne_zero_iff
deleted theorem norm_neg
added theorem norm_nonneg'
deleted theorem norm_nonneg
added theorem norm_of_add
added theorem norm_of_dual
added theorem norm_of_mul
added theorem norm_of_subsingleton'
deleted theorem norm_of_subsingleton
added theorem norm_one'
added theorem norm_pos_iff'''
added theorem norm_pos_iff''
deleted theorem norm_pos_iff'
deleted theorem norm_pos_iff
added theorem norm_prod_le
modified theorem norm_prod_le_iff
added theorem norm_prod_le_of_le
modified theorem norm_snd_le
deleted theorem norm_sub_eq_zero_iff
deleted theorem norm_sub_le
deleted theorem norm_sub_le_of_le
added theorem norm_sub_norm_le'
deleted theorem norm_sub_norm_le
deleted theorem norm_sub_pos_iff
deleted theorem norm_sub_rev
modified theorem norm_sum_le
deleted theorem norm_sum_le_of_le
added theorem norm_to_add
added theorem norm_to_dual
added theorem norm_to_mul
added theorem norm_to_nnreal'
deleted theorem norm_to_nnreal
deleted theorem norm_zero
added theorem pi.nnnorm_def'
deleted theorem pi.nnnorm_def
added theorem pi.norm_def'
deleted theorem pi.norm_def
deleted theorem pi.sum_norm_apply_le_norm
added theorem pi_nnnorm_const'
deleted theorem pi_nnnorm_const
added theorem pi_nnnorm_le_iff'
deleted theorem pi_nnnorm_le_iff
added theorem pi_nnnorm_lt_iff'
deleted theorem pi_nnnorm_lt_iff
added theorem pi_norm_const'
deleted theorem pi_norm_const
added theorem pi_norm_le_iff'
deleted theorem pi_norm_le_iff
added theorem pi_norm_lt_iff'
deleted theorem pi_norm_lt_iff
deleted theorem preimage_add_ball
deleted theorem preimage_add_closed_ball
deleted theorem preimage_add_sphere
added theorem preimage_mul_ball
added theorem preimage_mul_sphere
deleted theorem prod.nnnorm_def
added theorem prod.nnorm_def
added theorem squeeze_one_norm'
added theorem squeeze_one_norm
deleted theorem squeeze_zero_norm'
deleted theorem squeeze_zero_norm
added theorem subgroup.coe_norm
added theorem subgroup.norm_coe
modified theorem submodule.coe_norm
modified theorem submodule.norm_coe
added theorem tendsto_norm'
deleted theorem tendsto_norm
added theorem tendsto_norm_div_self
added theorem tendsto_norm_one
deleted theorem tendsto_norm_sub_self
deleted theorem tendsto_norm_zero
modified theorem ulift.nnnorm_def
added theorem ulift.nnnorm_down
modified theorem ulift.nnnorm_up
modified theorem ulift.norm_def
added theorem ulift.norm_down
modified theorem ulift.norm_up
deleted theorem uniform_continuous_nnnorm
deleted theorem uniform_continuous_norm