analyticOrderAt_add_eq_right_of_lt

English

Let f and g be analytic at z0. If the analytic order of g at z0 is strictly less than the analytic order of f at z0, then the analytic order of f+g at z0 equals the order of g.

Русский

Пусть f и g аналитичны в окрестности z0. Если порядок g в z0 строго меньше порядка f в z0, то порядок f+g в z0 равен порядку g.

LaTeX

$$$analyticOrderAt\, g\, z_0 < analyticOrderAt\, f\, z_0 \;\implies\; analyticOrderAt\,(f+g)\, z_0 = analyticOrderAt\, g\, z_0$$$

Lean4

theorem analyticOrderAt_add_eq_right_of_lt (hgf : analyticOrderAt g z₀ < analyticOrderAt f z₀) :
    analyticOrderAt (f + g) z₀ = analyticOrderAt g z₀ := by rw [add_comm, analyticOrderAt_add_eq_left_of_lt hgf]

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