Commit 2022-06-04 13:17 2a9be5b5

feat(analysis/special_functions): lemmas about filter map/comap (#14513)

• add comap_inf_principal_range and comap_nhds_within_range;
• add @[simp] to real.comap_exp_nhds_within_Ioi_zero;
• add real.comap_exp_nhds_zero, complex.comap_exp_comap_abs_at_top, complex.comap_exp_nhds_zero, complex.comap_exp_nhds_within_zero, and complex.tendsto_exp_nhds_zero_iff;
• add complex.map_exp_comap_re_at_bot and complex.map_exp_comap_re_at_top;
• add comap_norm_nhds_zero and complex.comap_abs_nhds_zero.