31 lines
748 B
Lean4
31 lines
748 B
Lean4
import Mathlib.Analysis.Analytic.Meromorphic
|
||
import Nevanlinna.analyticAt
|
||
import Nevanlinna.divisor
|
||
import Nevanlinna.meromorphicAt
|
||
import Nevanlinna.meromorphicOn_divisor
|
||
import Nevanlinna.stronglyMeromorphicOn
|
||
import Nevanlinna.mathlibAddOn
|
||
|
||
open scoped Interval Topology
|
||
open Real Filter MeasureTheory intervalIntegral
|
||
|
||
theorem MeromorphicOn.order_ne_top
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
(h₁U : IsConnected U)
|
||
(h₁f : MeromorphicOn f U) :
|
||
(∃ z₀ : U, (h₁f z₀.1 z₀.2).order = ⊤) ↔ (∀ z : U, (h₁f z.1 z.2).order = ⊤) := by
|
||
|
||
constructor
|
||
· intro h
|
||
obtain ⟨h₁z₀, h₂z₀⟩ := h
|
||
intro hz
|
||
|
||
|
||
sorry
|
||
|
||
· intro h
|
||
obtain ⟨w, hw⟩ := h₁U.nonempty
|
||
use ⟨w, hw⟩
|
||
exact h ⟨w, hw⟩
|