English
On a connected domain U, there exists a point with finite order iff every point has finite order.
Русский
На связном множестве U существует точка с конечным порядком тогда и только тогда, когда в каждой точке порядок конечен.
LaTeX
$$$\\exists u\\in U:\\, meromorphicOrderAt f u \\neq \\top \\quad\\Longleftrightarrow\\quad \\forall u\\in U:\\, meromorphicOrderAt f u \\neq \\top$$$
Lean4
/-- On a connected set, there exists a point where a meromorphic function `f` has finite order iff
`f` has finite order at every point. -/
theorem exists_meromorphicOrderAt_ne_top_iff_forall (hf : MeromorphicOn f U) (hU : IsConnected U) :
(∃ u : U, meromorphicOrderAt f u ≠ ⊤) ↔ (∀ u : U, meromorphicOrderAt f u ≠ ⊤) :=
by
constructor
· intro h₂f
have := isPreconnected_iff_preconnectedSpace.1 hU.isPreconnected
rcases isClopen_iff.1 hf.isClopen_setOf_meromorphicOrderAt_eq_top with h | h
· intro u
have : u ∉ (∅ : Set U) := by exact fun a => a
rw [← h] at this
tauto
· obtain ⟨u, hU⟩ := h₂f
have : u ∈ univ := by trivial
rw [← h] at this
tauto
· intro h₂f
obtain ⟨v, hv⟩ := hU.nonempty
use ⟨v, hv⟩, h₂f ⟨v, hv⟩
