toMeromorphicNFOn_eqOn_codiscrete

English

The normal form on U and the original function differ only on a codiscrete subset of U; outside this subset they agree.

Русский

Нормальная форма на U и исходная функция могут различаться только на кодискретной подмножине U; за пределами неё они совпадают.

LaTeX

$$$f =^{{\text{codiscreteWithin}}\,U}\ (toMeromorphicNFOn\ f\ U)$$$

Lean4

/-- Conversion to normal form on `U` changes the value only along a discrete subset
of `U`.
-/
theorem toMeromorphicNFOn_eqOn_codiscrete (hf : MeromorphicOn f U) :
    f =ᶠ[Filter.codiscreteWithin U] toMeromorphicNFOn f U :=
  by
  have : U ∈ Filter.codiscreteWithin U := by simp [mem_codiscreteWithin.2]
  filter_upwards [hf.analyticAt_mem_codiscreteWithin, this] with a h₁a h₂a
  simp [toMeromorphicNFOn, hf, ← (toMeromorphicNFAt_eq_self.2 h₁a.meromorphicNFAt).symm]

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