analyticOn — Mathlib

English

If a function is analytic on neighborhood sets around every point of s (AnalyticOnNhd), then it is analytic on s (AnalyticOn).

Русский

Если функция аналитична на окрестностях каждой точки множества s (AnalyticOnNhd), то она аналитична на множестве s (AnalyticOn).

LaTeX

$$$\text{AnalyticOnNhd}_{\mathcal{K}}(f,s) \Rightarrow \text{AnalyticOn}_{\mathcal{K}}(f,s)$$$

Lean4

theorem analyticOn (hf : AnalyticOnNhd 𝕜 f s) : AnalyticOn 𝕜 f s := fun x hx ↦ (hf x hx).analyticWithinAt

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