meromorphicNFOn_toMeromorphicNFOn

English

After applying the normal form transformation on U, the resulting function has a normal form on U: MeromorphicNFOn (toMeromorphicNFOn f U) U.

Русский

После применения преобразования в нормальную форму на U полученная функция имеет нормальную форму на U: MeromorphicNFOn (toMeromorphicNFOn f U) U.

LaTeX

$$$MeromorphicNFOn\ (toMeromorphicNFOn\ f\ U)\ U$$$

Lean4

/-- After conversion to normal form on `U`, the function has normal form.
-/
theorem meromorphicNFOn_toMeromorphicNFOn : MeromorphicNFOn (toMeromorphicNFOn f U) U :=
  by
  by_cases hf : MeromorphicOn f U
  · intro z hz
    rw [meromorphicNFAt_congr (toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds hf hz)]
    exact meromorphicNFAt_toMeromorphicNFAt
  · simpa [hf] using analyticOnNhd_const.meromorphicNFOn

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