English
The sum order obeys the minimum rule: meromorphicOrderAt(f1+f2) x ≥ min(meromorphicOrderAt f1 x, meromorphicOrderAt f2 x).
Русский
Порядок суммы удовлетворяет неравенству минимума: meromorphicOrderAt(f1+f2) x ≥ min(meromorphicOrderAt f1 x, meromorphicOrderAt f2 x).
LaTeX
$$$\\operatorname{meromorphicOrderAt}(f_1 + f_2) x \\geq \\min( \\operatorname{meromorphicOrderAt} f_1 x, \\operatorname{meromorphicOrderAt} f_2 x )$$$
Lean4
theorem eventually_analyticAt_or_mem_compl (h : MeromorphicOn f U) (hx : x ∈ U) :
∀ᶠ y in 𝓝[≠] x, AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ :=
by
have : { x }ᶜ = (U \ { x }) ∪ Uᶜ := by aesop (add simp Classical.em)
rw [this, nhdsWithin_union]
simp only [mem_compl_iff, eventually_sup]
refine ⟨?_, ?_⟩
· filter_upwards [h.eventually_analyticAt hx] with y hy using Or.inl hy
· filter_upwards [self_mem_nhdsWithin] with y hy using Or.inr hy
