diff --git a/Nevanlinna/meromorphicOn.lean b/Nevanlinna/meromorphicOn.lean index d88a1c9..01d1559 100644 --- a/Nevanlinna/meromorphicOn.lean +++ b/Nevanlinna/meromorphicOn.lean @@ -9,6 +9,31 @@ import Nevanlinna.mathlibAddOn open scoped Interval Topology open Real Filter MeasureTheory intervalIntegral +theorem MeromorphicOn.open_of_order_eq_top + {f : ℂ → ℂ} + {U : Set ℂ} + (h₁f : MeromorphicOn f U) : + IsOpen { u : U | (h₁f u.1 u.2).order = ⊤ } := by + + apply isOpen_iff_forall_mem_open.mpr + intro z hz + simp at hz + rw [MeromorphicAt.order_eq_top_iff] at hz + rw [eventually_nhdsWithin_iff] at hz + rw [eventually_nhds_iff] at hz + obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz + let t := + have : t ⊆ { u : U | (h₁f u.1 u.2).order = ⊤} := by + sorry + + + + rw [← eventually_eventually_nhds] at hz + + + sorry + + theorem MeromorphicOn.order_ne_top {f : ℂ → ℂ} {U : Set ℂ}