Theorem: ContinuousOn_uderiv (RMT4/Spaces.lean)

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ ContinuousOn uderiv (𝓗 U)
Tactic:
rintro f -
State after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ ContinuousWithinAt uderiv (𝓗 U) f

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ ContinuousWithinAt uderiv (𝓗 U) f
Tactic:
refine (tendsto_𝓒_iff hU).2 ?_
State after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ TendstoLocallyUniformlyOn uderiv (uderiv f) (𝓝[𝓗 U] f) U

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ TendstoLocallyUniformlyOn uderiv (uderiv f) (𝓝[𝓗 U] f) U
Tactic:
refine TendstoLocallyUniformlyOn.deriv ?_ eventually_mem_nhdsWithin hU
State after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ TendstoLocallyUniformlyOn (fun f => f) f (𝓝[𝓗 U] f) U

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ TendstoLocallyUniformlyOn (fun f => f) f (𝓝[𝓗 U] f) U
Tactic:
apply (tendsto_𝓒_iff hU).1
State after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ Tendsto (fun f => f) (𝓝[𝓗 U] f) (𝓝 f)

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ Tendsto (fun f => f) (𝓝[𝓗 U] f) (𝓝 f)
Tactic:
exact nhdsWithin_le_nhds
State after:
no goals