analyticOrderAt_mul_eq_top_of_right

English

If the analytic order of g at z0 is infinite, then the analytic order of f·g at z0 is infinite.

Русский

Если порядок g бесконечен в z0, то порядок f·g бесконечен в z0.

LaTeX

$$$analyticOrderAt\, g\, z_0 = \top \;\Rightarrow\; analyticOrderAt\,(f \cdot g)\, z_0 = \top$$$

Lean4

theorem analyticOrderAt_mul_eq_top_of_right (hg : analyticOrderAt g z₀ = ⊤) : analyticOrderAt (f * g) z₀ = ⊤ :=
  analyticOrderAt_smul_eq_top_of_right hg

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