toMeromorphicNFOn_eq_self_on_compl

English

If f is meromorphic on U, then its normal form on U agrees with f on the complement of U; i.e., outside U the two definitions coincide.

Русский

Если функция f мероморфна на множестве U, то нормальная форма на U совпадает с f за пределами U; то есть вне U две функции совпадают.

LaTeX

$$$\forall x \notin U,\ (toMeromorphicNFOn\ f\ U)(x) = f(x)$$$

Lean4

/-- Conversion to normal form on `U` does not change values outside of `U`.
-/
@[simp]
theorem toMeromorphicNFOn_eq_self_on_compl (hf : MeromorphicOn f U) : Set.EqOn (toMeromorphicNFOn f U) f Uᶜ :=
  by
  intro x hx
  simp_all [toMeromorphicNFOn]

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