AnalyticOnNhd — Mathlib

English

A function is analytic on a set if it is analytic around every point of that set.

Русский

Функция аналитична на множестве, если она аналитична в окрестности каждой точки этого множества.

LaTeX

$$$ AnalyticOn 𝕜 f s := \forall x \in s, AnalyticWithinAt 𝕜 f s x $$$

Lean4

/-- Given a function `f : E → F`, we say that `f` is analytic on a set `s` if it is analytic around
every point of `s`. -/
def AnalyticOnNhd (f : E → F) (s : Set E) :=
  ∀ x, x ∈ s → AnalyticAt 𝕜 f x

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