analyticOrderAt_smul_eq_top_of_left

English

If f is identically zero in a neighborhood of z0 (order infinite) then the product f·g is also of infinite order at z0.

Русский

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

LaTeX

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

Lean4

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

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