meromorphicOrderAt_toMeromorphicNFOn

English

The meromorphic order at x is unchanged by passing to the normal form on U: meromorphicOrderAt (toMeromorphicNFOn f U) x = meromorphicOrderAt f x.

Русский

Порядок мероморфности в точке x не меняется при переходе к нормальной форме на U: meromorphicOrderAt (toMeromorphicNFOn f U) x = meromorphicOrderAt f x.

LaTeX

$$$meromorphicOrderAt (toMeromorphicNFOn\ f\ U)\ x = meromorphicOrderAt\ f\ x$$$

Lean4

/-- Conversion of normal form does not affect orders.
-/
@[simp]
theorem meromorphicOrderAt_toMeromorphicNFOn (hf : MeromorphicOn f U) (hx : x ∈ U) :
    meromorphicOrderAt (toMeromorphicNFOn f U) x = meromorphicOrderAt f x :=
  by
  apply meromorphicOrderAt_congr
  exact hf.toMeromorphicNFOn_eq_self_on_nhdsNE hx

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