pi — Mathlib · SciLib

English

If every coordinate function f_i is analytic within a set s at a point e, then the joint map x ↦ (f_i(x)) is analytic within s at e.

Русский

Если каждая функция-координата f_i аналитична внутри множества s в точке e, то объединённое отображение x ↦ (f_i(x)) аналитично внутри s в e.

LaTeX

$$$\big(\forall i,\text{AnalyticWithinAt}_{\mathbb{k}}(f_i\,s\,e)\big) \,\Rightarrow\, \text{AnalyticWithinAt}_{\mathbb{k}}(\lambda x. (f \cdot x))\,s\,e$$$

Lean4

theorem pi (hf : ∀ i, AnalyticWithinAt 𝕜 (f i) s e) : AnalyticWithinAt 𝕜 (fun x ↦ (f · x)) s e :=
  by
  choose p hp using hf
  exact ⟨FormalMultilinearSeries.pi p, HasFPowerSeriesWithinAt.pi hp⟩

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