Update holomorphic_primitive2.lean

This commit is contained in:
Stefan Kebekus 2024-08-07 09:24:55 +02:00
parent c3289f89c7
commit ad5e7c69fd
1 changed files with 6 additions and 1 deletions

View File

@ -258,7 +258,12 @@ theorem primitive_hasDerivAtBasepoint
HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
let g := f ∘ fun z ↦ z + z₀
have : Continuous g := by continuity
have : ContinuousAt g 0 := by
apply ContinuousAt.comp
simpa
apply ContinuousAt.add
exact fun ⦃U⦄ a => a
exact continuousAt_const
let A := primitive_fderivAtBasepointZero g this
simp at A