English
The order of a sum is at least the minimum of the summand orders (repeated statement of the bound).
Русский
Порядок суммы не меньше минимума порядков слагаемых.
LaTeX
$$$\\min\\bigl( \\operatorname{meromorphicOrderAt} f_1 x, \\operatorname{meromorphicOrderAt} f_2 x \\bigr) \\leq \\operatorname{meromorphicOrderAt} (f_1 + f_2) x$$$
Lean4
/-- If two meromorphic functions have unequal orders, then the order of their sum is
exactly the minimum of the orders of the summands.
-/
theorem meromorphicOrderAt_add_of_ne (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x)
(h : meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x) :
meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) :=
by
rcases lt_or_lt_iff_ne.mpr h with h | h
· simpa [h.le] using meromorphicOrderAt_add_eq_left_of_lt hf₂ h
· simpa [h.le] using meromorphicOrderAt_add_eq_right_of_lt hf₁ h
