analyticAt — Mathlib

English

The analyticOn property holds if a function is analytic on a set by virtue of analyticity on each point of the set; specifically, for any s, AnalyticOn 𝕜 f s means f is analytic at every x ∈ s.

Русский

Свойство аналитичности на множестве означает AnalyticOn 𝕜 f s: функция аналитична в каждой точке множества.

LaTeX

$$$ AnalyticOn 𝕜 f s \;\text{means}\; \forall x\in s, \ AnalyticAt 𝕜 f x$$$

Lean4

protected theorem analyticAt (f : E →L[𝕜] F) (x : E) : AnalyticAt 𝕜 f x :=
  (f.hasFPowerSeriesAt x).analyticAt

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