mathlib3
2a9be5b5 - feat(analysis/special_functions): lemmas about filter `map`/`comap` (#14513)

Commit
3 years ago
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`.
Author
Parents
Loading