English
Analyticity around a point within a set is captured by having a power series valid in a neighborhood of the point restricted to that set.
Русский
Аналитичность вокруг точки внутри множества задается существованием степенного ряда в окрестности этой точки, ограниченной множеством.
LaTeX
$$$ AnalyticWithinAt 𝕜 f s x := \exists p, HasFPowerSeriesWithinAt f p s x $$$
Lean4
/-- `f` is analytic within `s` if it is analytic within `s` at each point of `s`. Note that
this is weaker than `AnalyticOnNhd 𝕜 f s`, as `f` is allowed to be arbitrary outside `s`. -/
def AnalyticOn (f : E → F) (s : Set E) : Prop :=
∀ x ∈ s, AnalyticWithinAt 𝕜 f s x
