mathlib3

2cf3ee29 - feat(analysis/calculus/cont_diff_def): no continuity is needed for has_ftaylor_series_up_to if n = ∞ (#18808)

feat(analysis/calculus/cont_diff_def): no continuity is needed for has_ftaylor_series_up_to if n = ∞ (#18808) We also add `has_ftaylor_series_up_to_iff_top` in order that the notation is consistent between `has_ftaylor_series_up_to` and `has_ftaylor_series_up_to_on`.