analyticOrderAt_ne_top_of_isPreconnected

English

On a preconnected set, if the order of f at some point is finite, then the order at any other point is also finite.

Русский

На предсвязанной совокупности, если в одной точке порядок конечен, то и в любой другой точке он конечен.

LaTeX

$$$\text{If } x,y \in U, \text{ with } U \text{ preconnected, and } analyticOrderAt f x \neq \top, \text{ then } analyticOrderAt f y \neq \top.$$$

Lean4

/-- On a preconnected set, a meromorphic function has finite order at one point if it has finite
order at another point. -/
theorem analyticOrderAt_ne_top_of_isPreconnected {x y : 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U)
    (h₁x : x ∈ U) (hy : y ∈ U) (h₂x : analyticOrderAt f x ≠ ⊤) : analyticOrderAt f y ≠ ⊤ :=
  (hf.exists_analyticOrderAt_ne_top_iff_forall ⟨nonempty_of_mem h₁x, hU⟩).1 (by use ⟨x, h₁x⟩) ⟨y, hy⟩

Похожие утверждения