mathlib3

34c828da - feat(topology/continuous_on): add `tendsto_nhds_within_iff` (#17260)

feat(topology/continuous_on): add `tendsto_nhds_within_iff` (#17260) We already had lemmas for both directions. This PR only packages them in an equivalence. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>