Commit 2024-09-26 10:19 5d4532a2

View on Github →

chore: rename AnalyticOn to AnalyticOnNhd, and AnalyticWithinOn to AnalyticOn (#17146) For coherence with ContinuousOn, DifferentiableOn and so on. See Zulip https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/Integrate.20analytic.20functions.20in.20the.20smooth.20hierarchy/near/471899268 This is 90% renaming all AnalyticOn to AnalyticOnNhd and then AnalyticWithinOn to AnalyticOn, and then adding deprecations. The 10% remaining is, when adding a deprecation alias AnalyticOn.foo := AnalyticOnNhd.foo, I noticed that AnalyticOn.foo would definitely make sense (with the new meaning of AnalyticOn), so I added the lemma with the new meaning instead of deprecating the old one.

Estimated changes

deleted theorem AnalyticOn.congr'
modified theorem AnalyticOn.congr
deleted theorem AnalyticOn.continuous
modified theorem AnalyticOn.mono
modified def AnalyticOn
added theorem AnalyticOnNhd.congr'
added theorem AnalyticOnNhd.congr
added theorem AnalyticOnNhd.mono
added def AnalyticOnNhd
deleted theorem AnalyticWithinOn.congr
deleted theorem AnalyticWithinOn.mono
deleted def AnalyticWithinOn
added theorem analyticOnNhd_congr'
added theorem analyticOnNhd_congr
deleted theorem analyticOn_congr'
deleted theorem analyticOn_congr
added theorem analyticOn_univ
deleted theorem analyticWithinOn_univ
deleted theorem AnalyticOn.comp'
modified theorem AnalyticOn.comp
added theorem AnalyticOnNhd.comp'
added theorem AnalyticOnNhd.comp
deleted theorem AnalyticWithinOn.comp
modified theorem AnalyticOn.comp₂
modified theorem AnalyticOn.curry_left
modified theorem AnalyticOn.curry_right
modified theorem AnalyticOn.inv
modified theorem AnalyticOn.mul
modified theorem AnalyticOn.smul
added theorem AnalyticOnNhd.add
added theorem AnalyticOnNhd.comp₂
added theorem AnalyticOnNhd.div
added theorem AnalyticOnNhd.inv
added theorem AnalyticOnNhd.mul
added theorem AnalyticOnNhd.neg
added theorem AnalyticOnNhd.pi
added theorem AnalyticOnNhd.pow
added theorem AnalyticOnNhd.prod
added theorem AnalyticOnNhd.smul
added theorem AnalyticOnNhd.sub
deleted theorem AnalyticWithinOn.add
deleted theorem AnalyticWithinOn.comp₂
deleted theorem AnalyticWithinOn.div
deleted theorem AnalyticWithinOn.inv
deleted theorem AnalyticWithinOn.mul
deleted theorem AnalyticWithinOn.neg
deleted theorem AnalyticWithinOn.pi
deleted theorem AnalyticWithinOn.pow
deleted theorem AnalyticWithinOn.prod
deleted theorem AnalyticWithinOn.smul
deleted theorem AnalyticWithinOn.sub
added theorem analyticOnNhd_const
added theorem analyticOnNhd_inv
added theorem analyticOnNhd_pi_iff
modified theorem analyticOn_inv
deleted theorem analyticWithinOn_const
deleted theorem analyticWithinOn_pi_iff
added theorem analyticOnNhd_fst
added theorem analyticOnNhd_id
added theorem analyticOnNhd_snd
deleted theorem analyticWithinOn_fst
deleted theorem analyticWithinOn_id
deleted theorem analyticWithinOn_snd
deleted theorem AnalyticOn.meromorphicOn
deleted theorem AnalyticOn.eval_linearMap
modified theorem AnalyticOn.contDiffOn
deleted theorem AnalyticOn.deriv
deleted theorem AnalyticOn.fderiv
deleted theorem AnalyticOn.iteratedFDeriv
deleted theorem AnalyticOn.iterated_deriv
added theorem AnalyticOnNhd.deriv
added theorem AnalyticOnNhd.fderiv
added theorem AnalyticOnNhd.cexp
added theorem AnalyticOnNhd.clog
added theorem AnalyticOnNhd.cpow
added theorem AnalyticWithinAt.cexp
added theorem AnalyticWithinAt.clog
added theorem AnalyticWithinAt.cpow
added theorem analyticOnNhd_cexp
modified theorem analyticOn_cexp
added theorem LSeries_analyticOnNhd