le_analyticOrderAt_sub — Mathlib

English

The order of a difference is at least the minimum of the orders of the summands.

Русский

Порядок разности не меньше минимума порядков слагаемых.

LaTeX

$$$\min(\operatorname{analyticOrderAt} f z_0, \operatorname{analyticOrderAt} g z_0) \le \operatorname{analyticOrderAt} (f - g) z_0$$$

Lean4

theorem le_analyticOrderAt_sub : min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f - g) z₀ := by
  simpa [sub_eq_add_neg] using le_analyticOrderAt_add (f := f) (g := -g)

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