Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-29 10:48 a630444a

View on Github →

feat(analysis/analytic/isolated_zeros): the uniqueness theorem for analytic fns (#16489)

Estimated changes

Modified src/analysis/analytic/basic.lean

added theorem analytic_at_const

added theorem analytic_on.add

added theorem analytic_on.sub

added theorem analytic_on_const

added theorem formal_multilinear_series.const_formal_multilinear_series_radius

added theorem has_fpower_series_at_const

added theorem has_fpower_series_on_ball_const

Modified src/analysis/analytic/isolated_zeros.lean

added theorem analytic_at.frequently_zero_iff_eventually_zero

added theorem analytic_on.eq_on_of_preconnected_of_frequently_eq'

added theorem analytic_on.eq_on_of_preconnected_of_frequently_eq

added theorem analytic_on.eq_on_of_preconnected_of_mem_closure'

added theorem analytic_on.eq_on_of_preconnected_of_mem_closure

Modified src/analysis/calculus/formal_multilinear_series.lean

added def const_formal_multilinear_series

added theorem const_formal_multilinear_series_apply

Modified src/topology/continuous_on.lean

added theorem frequently_nhds_within_iff

added theorem mem_closure_ne_iff_frequently_within

Modified src/topology/separation.lean

added theorem is_open_set_of_eventually_nhds_within