analyticOnNhd — Mathlib

English

A function is ContDiff of all orders if and only if it is AnalyticOnNhd on univ; in particularomega-analytic equivalence.

Русский

Функция обладает гладкостью для всех порядков тогда и только тогда, когда она аналитична в окрестностях на.univ; равносильность с аналитикой на окрестности.

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{K}}\omega\ f \iff \operatorname{AnalyticOnNhd}_{\mathbb{K}}\ f\ univ$$$

Lean4

theorem analyticOnNhd (h : ContDiff 𝕜 ω f) : AnalyticOnNhd 𝕜 f s :=
  by
  rw [← contDiffOn_univ] at h
  have := h.analyticOn
  rw [analyticOn_univ] at this
  exact this.mono (subset_univ _)

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