contDiff_omega_iff_analyticOnNhd — Mathlib

English

Same as above: ContDiff 𝕜 ω f if and only if AnalyticOnNhd 𝕜 f univ.

Русский

То же самое: ContDiff 𝕜 ω f тогда и только тогда, когда AnalyticOnNhd 𝕜 f univ.

LaTeX

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

Lean4

theorem contDiff_omega_iff_analyticOnNhd : ContDiff 𝕜 ω f ↔ AnalyticOnNhd 𝕜 f univ :=
  ⟨fun h ↦ h.analyticOnNhd, fun h ↦ h.contDiff⟩

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