analyticOnNhd — Mathlib

English

AnalyticOnNhd 𝕜 f s holds if at every x ∈ s the function is analytic in a neighborhood of x; in particular, f is analytic at every x in s.

Русский

AnalyticOnNhd 𝕜 f s означает, что в каждой точке x∈s функция аналитична в окрестности x; следовательно, f аналитична в каждой точке s.

LaTeX

$$$ AnalyticOnNhd 𝕜 f s$$$

Lean4

protected theorem analyticOnNhd (f : E →L[𝕜] F) (s : Set E) : AnalyticOnNhd 𝕜 f s := fun x _ ↦ f.analyticAt x

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