meromorphicOrderAt_add_eq_right_of_lt

English

If meromorphic orders are not equal, then the order of the sum equals the minimum of the two orders.

Русский

Если порядки не равны, то порядок суммы равен минимуму двух порядков.

LaTeX

$$$\\operatorname{meromorphicOrderAt}(f_1 + f_2) x = \\min\\bigl( \\operatorname{meromorphicOrderAt} f_1 x, \\operatorname{meromorphicOrderAt} f_2 x \\bigr)$$$

Lean4

/-- Helper lemma for meromorphicOrderAt_add_of_ne.
-/
theorem meromorphicOrderAt_add_eq_right_of_lt (hf₁ : MeromorphicAt f₁ x)
    (h : meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x) :
    meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₂ x :=
  by
  rw [add_comm]
  exact meromorphicOrderAt_add_eq_left_of_lt hf₁ h

Похожие утверждения