Commit 2023-09-04 07:35 04d2f7d8

View on Github →

fix(Analysis,Topology): fix names (#6938) Rename:

  • tendsto_iff_norm_tendsto_one → tendsto_iff_norm_div_tendsto_zero;
  • tendsto_iff_norm_tendsto_zero → tendsto_iff_norm_sub_tendsto_zero;
  • tendsto_one_iff_norm_tendsto_one → tendsto_one_iff_norm_tendsto_zero;
  • Filter.Tendsto.continuous_of_equicontinuous_at → Filter.Tendsto.continuous_of_equicontinuousAt.

Estimated changes