Theorem: ContinuousOn_obs (RMT4/Main.lean)

State before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
⊢ ContinuousOn (obs z₀) (𝓗 U)
Tactic:
have e1 : z₀ ∈ {z₀} := mem_singleton _
State after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
e1 : z₀ ∈ {z₀}
⊢ ContinuousOn (obs z₀) (𝓗 U)

State before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
e1 : z₀ ∈ {z₀}
⊢ ContinuousOn (obs z₀) (𝓗 U)
Tactic:
have e2 : {z₀} ∈ compacts U := ⟨singleton_subset_iff.2 hz₀, isCompact_singleton⟩
State after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
e1 : z₀ ∈ {z₀}
e2 : {z₀} ∈ compacts U
⊢ ContinuousOn (obs z₀) (𝓗 U)

State before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
e1 : z₀ ∈ {z₀}
e2 : {z₀} ∈ compacts U
⊢ ContinuousOn (obs z₀) (𝓗 U)
Tactic:
apply continuous_norm.comp_continuousOn
State after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
e1 : z₀ ∈ {z₀}
e2 : {z₀} ∈ compacts U
⊢ ContinuousOn (fun x => deriv x z₀) (𝓗 U)

State before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
e1 : z₀ ∈ {z₀}
e2 : {z₀} ∈ compacts U
⊢ ContinuousOn (fun x => deriv x z₀) (𝓗 U)
Tactic:
exact (UniformOnFun.uniformContinuous_eval_of_mem _ _ e1 e2).continuous.comp_continuousOn
  (ContinuousOn_uderiv hU)
State after:
no goals