English
If meromorphicOrderAt f1 x < meromorphicOrderAt f2 x, then meromorphicOrderAt(f1+f2) x = meromorphicOrderAt f1 x.
Русский
Если meromorphicOrderAt f1 x < meromorphicOrderAt f2 x, то meromorphicOrderAt(f1+f2) x = meromorphicOrderAt f1 x.
LaTeX
$$$\\text{If } \\operatorname{meromorphicOrderAt} f_1 x < \\operatorname{meromorphicOrderAt} f_2 x, \\ \\operatorname{meromorphicOrderAt} (f_1+f_2) x = \\operatorname{meromorphicOrderAt} f_1 x$$$
Lean4
/-- Meromorphic functions on `U` are analytic on `U`, outside of a discrete subset. -/
theorem analyticAt_mem_codiscreteWithin (hf : MeromorphicOn f U) : {x | AnalyticAt 𝕜 f x} ∈ Filter.codiscreteWithin U :=
by
rw [mem_codiscreteWithin]
intro x hx
rw [Filter.disjoint_principal_right, ← Filter.eventually_mem_set]
filter_upwards [hf.eventually_analyticAt_or_mem_compl hx] with y hy
simp
tauto
