analyticAt_iff_analytic_smul — Mathlib

English

If f is analytic at z and f(z) ≠ 0, then AnalyticAt g z is equivalent to AnalyticAt (f · g) z.

Русский

Если f аналитична в z и f(z) ≠ 0, то AnalyticAt g z эквивалентно AnalyticAt (f·g) z.

LaTeX

$$$\mathit{AnalyticAt}_{\mathfrak k}(f,z) \land f(z) \neq 0 \Rightarrow \bigl( \mathit{AnalyticAt}_{\mathfrak k}(g,z) \iff \mathit{AnalyticAt}_{\mathfrak k}\bigl(\lambda w. f(w)\,g(w)\bigr)(z) \bigr).$$$

Lean4

theorem analyticAt_iff_analytic_smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E}
    (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) : AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f • g) z :=
  analyticAt_iff_analytic_fun_smul h₁f h₂f

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