The codiscrete ⇄ punctured-neighborhood bridge (D2) and the identity dichotomy

Unit: meromorphic-and-divisors (docs/design/meromorphic-and-divisors.md §4.2, proof plan §6.1).

• mem_codiscreteWithin_iff_of_isOpen / eventuallyEq_codiscreteWithin_iff_of_isOpen / eventually_codiscreteWithin_iff_of_isOpen: for open U, membership in codiscreteWithin U (equivalently: =ᶠ-agreement, or an eventual property) is purely topological — it holds pointwise on 𝓝[≠] x for every x ∈ U. This is the pivot that lets ord/evalAt/divisor descend to MeroGermOn classes against arbitrary representatives.
• codiscreteWithin_neBot, the instance (codiscrete X).NeBot.
• MeromorphicOnX.congr_codiscreteWithin, MeromorphicOnX.analyticAt_codiscreteWithin.
• The meromorphic identity dichotomy MeromorphicOnX.eventuallyEq_zero_or_forall_ordAtX_ne_top on a connected surface, and its corollary MeromorphicOnX.codiscrete_setOf_ne_zero — feeds Field (ℳ X) and divisor well-definedness.

D2: the bridge, both directions

theorem RS.mem_codiscreteWithin_iff_of_isOpen {X : Type u_1} [TopologicalSpace X] {U S : Set X} (hU : IsOpen U) : S ∈ Filter.codiscreteWithin U ↔ ∀ x ∈ U, S ∈ nhdsWithin x {x}ᶜ

theorem RS.eventuallyEq_codiscreteWithin_iff_of_isOpen {X : Type u_1} [TopologicalSpace X] {U : Set X} {α : Type u_2} {f g : X → α} (hU : IsOpen U) : f =ᶠ[Filter.codiscreteWithin U] g ↔ ∀ x ∈ U, f =ᶠ[nhdsWithin x {x}ᶜ] g

D2 (both directions): for open U, agreement of arbitrary f, g codiscretely within U is exactly pointwise 𝓝[≠]-agreement. Meromorphy-free.

theorem RS.eventually_codiscreteWithin_iff_of_isOpen {X : Type u_1} [TopologicalSpace X] {U : Set X} {p : X → Prop} (hU : IsOpen U) : (∀ᶠ (x : X) in Filter.codiscreteWithin U, p x) ↔ ∀ x ∈ U, ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, p y

Prop-valued version of the D2 bridge.

theorem RS.eventuallyEq_codiscrete_iff {X : Type u_1} [TopologicalSpace X] {α : Type u_2} {f g : X → α} : f =ᶠ[Filter.codiscrete X] g ↔ ∀ (x : X), f =ᶠ[nhdsWithin x {x}ᶜ] g

NeBot instances

theorem RS.codiscreteWithin_neBot {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} (hU : IsOpen U) (hne : U.Nonempty) : (Filter.codiscreteWithin U).NeBot

instance RS.instNeBotCodiscrete {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [Nonempty X] : (Filter.codiscrete X).NeBot

Congruence and analyticity off a codiscrete set

theorem RS.MeromorphicOnX.congr_codiscreteWithin {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {U : Set X} (hf : MeromorphicOnX f U) (hU : IsOpen U) (h : f =ᶠ[Filter.codiscreteWithin U] g) : MeromorphicOnX g U

theorem RS.MeromorphicOnX.analyticAt_codiscreteWithin {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {U : Set X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hf : MeromorphicOnX f U) (hU : IsOpen U) : ∀ᶠ (y : X) in Filter.codiscreteWithin U, AnalyticAt ℂ (f ∘ ↑(chartAt ℂ y).symm) (↑(chartAt ℂ y) y)

Meromorphic functions on an open set are chart-analytic off a set codiscrete in it.

The meromorphic identity dichotomy (§6.1)

theorem RS.MeromorphicOnX.eventuallyEq_zero_or_forall_ordAtX_ne_top {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} [T1Space X] [ConnectedSpace X] (hf : MeromorphicOnX f Set.univ) : f =ᶠ[Filter.codiscrete X] 0 ∨ ∀ (x : X), ordAtX f x ≠ ⊤

The meromorphic identity dichotomy on a connected surface: a function meromorphic everywhere is codiscretely zero, or nowhere locally-≡0. Both S := {ord = ⊤} and its complement are open (via eventually_ordAtX_eq_top / eventually_ordAtX_eq_zero), so connectedness forces S = ∅ or S = univ.

theorem RS.MeromorphicOnX.codiscrete_setOf_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} [T1Space X] [ConnectedSpace X] (hf : MeromorphicOnX f Set.univ) (h : ¬f =ᶠ[Filter.codiscrete X] 0) : ∀ᶠ (z : X) in Filter.codiscrete X, f z ≠ 0