eventually_codiscreteWithin_analyticAt

English

For a meromorphic function on U (with complete target space), the function is analytic on a codiscrete subset of U (i.e., analytic almost everywhere in the codiscrete sense).

Русский

Для мероморфной функции на U (с завершённым пространством назначения) она аналитична на кодискретной части U (почти везде в кодискретном смысле).

LaTeX

$$$\forall f:\mathbb{K}\to E,\ MeromorphicOn(f, U) \Rightarrow \text{(codiscreteWithin }U)\text{Almost surely AnalyticAt}$$$

Lean4

theorem eventually_codiscreteWithin_analyticAt [CompleteSpace E] (f : 𝕜 → E) (h : MeromorphicOn f U) :
    ∀ᶠ (y : 𝕜) in codiscreteWithin U, AnalyticAt 𝕜 f y :=
  by
  rw [eventually_iff, mem_codiscreteWithin]
  intro x hx
  rw [disjoint_principal_right]
  apply Filter.mem_of_superset ((h x hx).eventually_analyticAt)
  intro x hx
  simp [hx]

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