Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-11 04:03 bcd79a1f

View on Github →

chore(analysis/normed/group/basic): rename vars (#9652)

  • use E, F for (semi)normed groups and greek letters for other types;
  • golf some proofs (bounded_iff_forall_norm_le, norm_pos_iff');
  • use namespace lipschitz_with and namespace antilipschitz_with instead of manual prefixes for all lemmas;
  • generalize antilipschitz_with.add_lipschitz_with to pseudo_emetric_space;
  • add antilipschitz_with.edist_lt_top and antilipschitz_with.edist_ne_top;
  • fix a typo in pseudo_emetric_space.to_pseudo_metric_space.

Estimated changes

modified theorem abs_norm_sub_norm_le
modified theorem add_mem_ball_iff_norm
modified theorem ball_zero_eq
modified theorem bounded_iff_forall_norm_le
modified theorem cauchy_seq.add
modified theorem coe_neg_sphere
modified theorem coe_nnnorm
modified theorem continuous_nnnorm
modified theorem continuous_norm
modified theorem dist_add_add_le
modified theorem dist_add_add_le_of_le
modified theorem dist_add_left
modified theorem dist_add_right
modified theorem dist_eq_norm'
modified theorem dist_eq_norm
modified theorem dist_le_norm_add_norm
modified theorem dist_neg_neg
modified theorem dist_norm_norm_le
modified theorem dist_sub_left
modified theorem dist_sub_right
modified theorem dist_sub_sub_le
modified theorem dist_sub_sub_le_of_le
modified theorem dist_sum_sum_le
modified theorem dist_sum_sum_le_of_le
modified theorem dist_zero_left
modified theorem dist_zero_right
modified theorem edist_add_add_le
modified theorem edist_eq_coe_nnnorm
modified theorem edist_eq_coe_nnnorm_sub
modified theorem eq_of_norm_sub_eq_zero
modified theorem eq_of_norm_sub_le_zero
modified theorem filter.tendsto.norm
modified theorem is_bounded_under_of_tendsto
modified theorem isometric.add_left_symm
modified theorem isometric.add_left_to_equiv
modified theorem isometric.add_right_apply
modified theorem isometric.add_right_symm
modified theorem isometric.coe_add_left
modified theorem isometric.coe_add_right
modified theorem isometric.coe_neg
modified theorem isometric.neg_symm
modified theorem isometric.neg_to_equiv
modified theorem lipschitz_with.add
modified theorem lipschitz_with.neg
modified theorem lipschitz_with.sub
modified theorem lipschitz_with_one_norm
modified theorem mem_ball_iff_norm'
modified theorem mem_ball_iff_norm
modified theorem mem_ball_zero_iff
modified theorem mem_closed_ball_iff_norm'
modified theorem mem_closed_ball_iff_norm
modified theorem mem_emetric_ball_zero_iff
modified theorem mem_sphere_iff_norm
modified theorem mem_sphere_zero_iff_norm
modified theorem nat.norm_cast_le
modified theorem ne_zero_of_norm_pos
modified theorem nndist_add_add_le
modified theorem nndist_eq_nnnorm
modified theorem nndist_nnnorm_nnnorm_le
modified theorem nnnorm_add_le
modified theorem nnnorm_eq_zero
modified theorem nnnorm_neg
modified theorem nnnorm_sum_le
modified theorem nnnorm_zero
modified theorem nonzero_of_mem_sphere
modified theorem nonzero_of_mem_unit_sphere
modified theorem norm_add_le
modified theorem norm_add_le_of_le
modified theorem norm_eq_of_mem_sphere
modified theorem norm_eq_zero
modified theorem norm_eq_zero_iff'
modified theorem norm_fst_le
modified theorem norm_le_insert'
modified theorem norm_le_insert
modified theorem norm_le_of_mem_closed_ball
modified theorem norm_le_zero_iff'
modified theorem norm_le_zero_iff
modified theorem norm_lt_of_mem_ball
modified theorem norm_neg
modified theorem norm_nonneg
modified theorem norm_of_subsingleton
modified theorem norm_pos_iff'
modified theorem norm_pos_iff
modified theorem norm_prod_le_iff
modified theorem norm_snd_le
modified theorem norm_sub_eq_zero_iff
modified theorem norm_sub_le
modified theorem norm_sub_le_of_le
modified theorem norm_sub_norm_le
modified theorem norm_sub_rev
modified theorem norm_sum_le
modified theorem norm_sum_le_of_le
modified theorem norm_zero
modified theorem normed_group.cauchy_seq_iff
modified structure normed_group.core
modified def normed_group.induced
modified theorem of_real_norm_eq_coe_nnnorm
modified theorem pi_nnnorm_const
modified theorem pi_nnsemi_norm_const
modified theorem pi_norm_const
modified theorem pi_semi_norm_const
modified theorem preimage_add_ball
modified theorem preimage_add_closed_ball
modified theorem preimage_add_sphere
modified theorem prod.nnnorm_def
modified theorem prod.nnsemi_norm_def
modified theorem prod.norm_def
modified theorem prod.semi_norm_def
modified theorem semi_norm_fst_le
modified theorem semi_norm_prod_le_iff
modified theorem semi_norm_snd_le
modified structure semi_normed_group.core
modified theorem squeeze_zero_norm'
modified theorem squeeze_zero_norm
modified theorem tendsto_norm
modified theorem tendsto_norm_sub_self
modified theorem tendsto_norm_zero
modified theorem uniform_continuous_nnnorm
modified theorem uniform_continuous_norm