analyticWithinAt — Mathlib

English

Analytic within at x given a suitable neighborhood.

Русский

Аналитичность внутри в точке x при подходящем окрестности.

LaTeX

$$$\displaystyle \text{AnalyticWithinAt 𝕜 f s x}$$$

Lean4

theorem analyticWithinAt (h : ContDiffWithinAt 𝕜 ω f s x) : AnalyticWithinAt 𝕜 f s x :=
  by
  obtain ⟨u, hu, hf⟩ := h.analyticOn
  have xu : x ∈ u := mem_of_mem_nhdsWithin (by simp) hu
  exact (hf x xu).mono_of_mem_nhdsWithin (nhdsWithin_mono _ (subset_insert _ _) hu)

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