pi — Mathlib · SciLib

English

If each coordinate function f_i is analytic on a set s, then the joint map x ↦ (f_i(x)) is analytic on s.

Русский

Если каждая f_i аналитична на множестве s, то отображение x ↦ (f_i(x)) аналитично на s.

LaTeX

$$$(\forall i,\ AnalyticOn_{\mathbb{k}}(f_i)\,s) \Rightarrow \ AnalyticOn_{\mathbb{k}}(\lambda x. (f \cdot x))\,s$$$

Lean4

theorem pi (hf : ∀ i, AnalyticOn 𝕜 (f i) s) : AnalyticOn 𝕜 (fun x ↦ (f · x)) s := fun x hx ↦
  AnalyticWithinAt.pi (fun i ↦ hf i x hx)

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