Update holomorphic.primitive.lean

This commit is contained in:
Stefan Kebekus 2024-06-16 19:15:19 +02:00
parent bb74aa273f
commit 321ceba46b
1 changed files with 9 additions and 0 deletions

View File

@ -219,6 +219,15 @@ theorem primitive_fderivAtBasepoint
rw [Filter.eventually_iff_exists_mem]
let s := f⁻¹' Metric.ball (f 0) c
have : IsOpen s := by
apply IsOpen.mem_nhds
apply IsOpen.preimage hf
exact Metric.isOpen_ball
--sorry
--apply isOpen_iff_ball_subset
use s
constructor
· apply IsOpen.mem_nhds