clog — Mathlib

English

If f is analytic within a set and log is analytic around f, then log∘f is analytic within the set.

Русский

Если f аналитична внутри множества и log аналитичен рядом с f, то log∘f аналитична внутри множества.

LaTeX

$$$\\text{AnalyticWithinAt}(\\log \\circ f, s, x)$ from $\\text{AnalyticOn}.clog$$$

Lean4

theorem clog (fs : AnalyticOn ℂ f s) (m : ∀ z ∈ s, f z ∈ slitPlane) : AnalyticOn ℂ (fun z ↦ log (f z)) s := fun z n ↦
  (analyticAt_clog (m z n)).analyticWithinAt.comp (fs z n) m

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