English
The within-domain version of the above: the set of points in U where the order is 0 or ∞ is codiscreteWithin U.
Русский
Внутренний аналог: множество точек внутри U, где порядок 0 или ∞, кодискретно внутри U.
LaTeX
$$AnalyticOnNhd.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top$$
Lean4
/-- The set where an analytic function has zero or infinite order is discrete within its domain of
analyticity.
-/
theorem codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top (hf : AnalyticOnNhd 𝕜 f U) :
{u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤} ∈ codiscreteWithin U :=
by
simp_rw [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]
