English
On a connected domain, there exists a point where the analytic order is finite if and only if the analytic order is finite at every point.
Русский
На связной области существует точка с конечным порядком аналитической функции тогда и только тогда, когда конечен порядок во всех точках области.
LaTeX
$$(∃ u ∈ U, analyticOrderAt f u ≠ ∞) ↔ (∀ u ∈ U, analyticOrderAt f u ≠ ∞)$$
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_analyticOrderAt_ne_top_iff_forall (hf : AnalyticOnNhd 𝕜 f U) (hU : IsConnected U) :
(∃ u : U, analyticOrderAt f u ≠ ⊤) ↔ (∀ u : U, analyticOrderAt f u ≠ ⊤) :=
by
have : ConnectedSpace U := Subtype.connectedSpace hU
obtain ⟨v⟩ : Nonempty U := inferInstance
suffices (∀ (u : U), analyticOrderAt f u ≠ ⊤) ∨ ∀ (u : U), analyticOrderAt f u = ⊤ by tauto
simpa [Set.eq_empty_iff_forall_notMem, Set.eq_univ_iff_forall] using
isClopen_iff.1 hf.isClopen_setOf_analyticOrderAt_eq_top
