meromorphicOrderAt_ne_top_of_isPreconnected

English

If f is meromorphic on a preconnected set U, and x,y ∈ U with meromorphicOrderAt f x ≠ ⊤, then meromorphicOrderAt f y ≠ ⊤.

Русский

Если f мероморфна на предсвязном множестве U и x,y ∈ U так, что meromorphicOrderAt f x ≠ ⊤, то meromorphicOrderAt f y ≠ ⊤.

LaTeX

$$$\\text{If } \\text{IsPreconnected}(U) \\text{ and } x,y\\in U,\\ meromorphicOrderAt f x \\neq \\top \\Rightarrow meromorphicOrderAt 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 meromorphicOrderAt_ne_top_of_isPreconnected (hf : MeromorphicOn f U) {y : 𝕜} (hU : IsPreconnected U)
    (h₁x : x ∈ U) (hy : y ∈ U) (h₂x : meromorphicOrderAt f x ≠ ⊤) : meromorphicOrderAt f y ≠ ⊤ :=
  (hf.exists_meromorphicOrderAt_ne_top_iff_forall ⟨nonempty_of_mem h₁x, hU⟩).1 (by use ⟨x, h₁x⟩) ⟨y, hy⟩

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