English
The set of points where analyticOrderAt equals either 0 or infinity is codiscrete in the domain.
Русский
Множество точек, где аналитический порядок равен 0 или бесконечности, кодискретно в области определения.
LaTeX
$$The set {u ∈ U : analyticOrderAt f u ∈ {0, ∞}} is codiscrete in U.$$
Lean4
/-- The set where an analytic function has zero or infinite order is discrete within its domain of
analyticity. -/
theorem codiscrete_setOf_analyticOrderAt_eq_zero_or_top (hf : AnalyticOnNhd 𝕜 f U) :
{u : U | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤} ∈ Filter.codiscrete U :=
by
simp_rw [mem_codiscrete_subtype_iff_mem_codiscreteWithin, mem_codiscreteWithin, disjoint_principal_right]
intro x hx
rcases (hf x hx).eventually_eq_zero_or_eventually_ne_zero with h₁f | h₁f
· filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁f.eventually_nhds] with a ha
simp [analyticOrderAt_eq_top, ha]
· filter_upwards [h₁f] with a ha
simp +contextual [(hf a _).analyticOrderAt_eq_zero, ha]
