analyticOrderAt_smul_eq_top_of_right

English

If g satisfies infinite order at z0, then the product f·g has infinite order at z0.

Русский

Если функция g имеет бесконечный порядок в z0, то произведение f·g имеет бесконечный порядок в z0.

LaTeX

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

Lean4

theorem analyticOrderAt_smul_eq_top_of_right {f : 𝕜 → 𝕜} (hg : analyticOrderAt g z₀ = ⊤) :
    analyticOrderAt (f • g) z₀ = ⊤ :=
  by
  rw [analyticOrderAt_eq_top, eventually_nhds_iff] at *
  obtain ⟨t, h₁t, h₂t, h₃t⟩ := hg
  exact ⟨t, fun y hy ↦ by simp [h₁t y hy], h₂t, h₃t⟩

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