pi — Mathlib · SciLib

English

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

Русский

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

LaTeX

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

Lean4

theorem pi (hf : ∀ i, AnalyticAt 𝕜 (f i) e) : AnalyticAt 𝕜 (fun x ↦ (f · x)) e :=
  by
  simp_rw [← analyticWithinAt_univ] at hf ⊢
  exact AnalyticWithinAt.pi hf

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