analyticOrderAt_mul_eq_top_of_left

English

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

Русский

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

LaTeX

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

Lean4

theorem analyticOrderAt_mul_eq_top_of_left (hf : analyticOrderAt f z₀ = ⊤) : analyticOrderAt (f * g) z₀ = ⊤ :=
  analyticOrderAt_smul_eq_top_of_left hf

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