analyticWithinAt_pi_iff — Mathlib

English

The within-analytic statement for the joint map x ↦ (f_i(x)) with a pi-series is equivalent to the collection of within-analytic statements for each coordinate f_i.

Русский

Утверждение аналитичности внутри совместного отображения x ↦ (f_i(x)) эквивалентно набору локальных утверждений аналитичности для каждого f_i.

LaTeX

$$$HasFPowerSeriesWithinAt\,(\lambda x. (f \cdot x))\,(\mathrm{pi}\,p)\,s\,e \;\Longleftrightarrow\; \forall i, HasFPowerSeriesWithinAt\,(f_i)\,(p_i)\,e$$$

Lean4

theorem analyticWithinAt_pi_iff : AnalyticWithinAt 𝕜 (fun x ↦ (f · x)) s e ↔ ∀ i, AnalyticWithinAt 𝕜 (f i) s e :=
  by
  refine ⟨fun h i ↦ ?_, fun h ↦ .pi h⟩
  exact ((ContinuousLinearMap.proj (R := 𝕜) i).analyticAt _).comp_analyticWithinAt h

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