English
The codiscrete set property holds for the zero/infinite order under meromorphic order at equality; the codiscrete subset is stable under projection.
Русский
Свойство кодискретности сохраняется для нулевого/бесконечного порядка при мероморфном порядке.
LaTeX
$$$\\text{codiscrete setOf meromorphicOrderAtEqTop}$$$
Lean4
/-- The set where a meromorphic function has zero or infinite
order is codiscrete within its domain of meromorphicity. -/
theorem codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top (hf : MeromorphicOn f U) :
{u : U | meromorphicOrderAt f u = 0 ∨ meromorphicOrderAt f u = ⊤} ∈ Filter.codiscrete U :=
by
rw [mem_codiscrete_subtype_iff_mem_codiscreteWithin, mem_codiscreteWithin]
intro x hx
rw [Filter.disjoint_principal_right]
rcases (hf x hx).eventually_eq_zero_or_eventually_ne_zero with h₁f | h₁f
· filter_upwards [eventually_eventually_nhdsWithin.2 h₁f] with a h₁a
suffices ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0 by simp +contextual [meromorphicOrderAt_eq_top_iff, this]
obtain rfl | hax := eq_or_ne a x
· exact h₁a
rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at h₁a ⊢
obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₁a
use t \ { x }, fun y h₁y _ ↦ h₁t y h₁y.1 h₁y.2
exact ⟨h₂t.sdiff isClosed_singleton, Set.mem_diff_of_mem h₃t hax⟩
· filter_upwards [hf.eventually_analyticAt_or_mem_compl hx, h₁f] with a h₁a h'₁a
simp only [mem_compl_iff, mem_diff, mem_image, mem_setOf_eq, Subtype.exists, exists_and_right, exists_eq_right,
not_exists, not_or, not_and, not_forall, Decidable.not_not]
rcases h₁a with h' | h'
· simp +contextual [h'.meromorphicOrderAt_eq, h'.analyticOrderAt_eq_zero.2, h'₁a]
· exact fun ha ↦ (h' ha).elim
