9 lines
253 B
Lean4
9 lines
253 B
Lean4
import Mathlib
|
||
|
||
variable
|
||
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
|
||
|
||
lemma MeromorphicAt.comp {x : ℝ} {f : ℂ → E} {g : ℝ → ℂ}
|
||
(hf : MeromorphicAt f (g x)) (hg : AnalyticAt ℝ g x) : MeromorphicAt (f ∘ g) x := by
|
||
sorry
|