toMeromorphicNFOn_eq_toMeromorphicNFAt

English

For x ∈ U, the value of the global normal form at x is the same as the local normal form at x, i.e., (toMeromorphicNFOn f U) x = (toMeromorphicNFAt f x x).

Русский

Для x ∈ U значение глобальной нормальной формы в точке совпадает с локальной формой в этой точке: (toMeromorphicNFOn f U) x = (toMeromorphicNFAt f x x).

LaTeX

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

Lean4

/-- If `f` is meromorphic on `U` and `x ∈ U`, then conversion to normal form at `x`
and conversion to normal form on `U` agree at `x`.
-/
theorem toMeromorphicNFOn_eq_toMeromorphicNFAt (hf : MeromorphicOn f U) (hx : x ∈ U) :
    toMeromorphicNFOn f U x = toMeromorphicNFAt f x x :=
  by
  apply Filter.EventuallyEq.eq_of_nhds (g := toMeromorphicNFAt f x)
  simp [(toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds hf hx).trans]

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