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