eqOn_compl_singleton_toMeromorphicNFAt

English

Conversion to normal form at x changes the value only at x.

Русский

Преобразование к нормальной форме в точке x изменяет значение только в x.

LaTeX

$$$Set.EqOn\ f\ (toMeromorphicNFAt\ f\ x)\ { x }^{c}$$$

Lean4

/-- Conversion to normal form at `x` changes the value only at x. -/
theorem eqOn_compl_singleton_toMeromorphicNFAt (hf : MeromorphicAt f x) : Set.EqOn f (toMeromorphicNFAt f x) { x }ᶜ :=
  fun _ _ ↦ by simp_all [toMeromorphicNFAt]

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