analyticAt_iff_analytic_fun_mul — Mathlib

English

Let f be analytic at z with f(z) ≠ 0. Then AnalyticAt g z is equivalent to AnalyticAt (f(z) · g(z)) at z.

Русский

Пусть f аналитична в z и f(z) ≠ 0. Тогда AnalyticAt g z эквивалентно AnalyticAt (f(z) · g(z)) в 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_fun_mul {f g : E → 𝕝} {z : E} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) :
    AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (fun z ↦ f z * g z) z :=
  by
  simp_rw [← smul_eq_mul]
  exact analyticAt_iff_analytic_smul h₁f h₂f

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