pi — Mathlib · SciLib

English

Near-point analytic property: the joint map is analytic in a neighborhood iff each coordinate is analytic in a neighborhood.

Русский

Пусть для каждого i f_i аналитична в некоторой окрестности; тогда совместное отображение аналитично в этой окрестности.

LaTeX

$$$\text{AnalyticOnNhd}_{\mathbb{k}}(\lambda x. (f \cdot x))\,s \iff \forall i, \text{AnalyticOnNhd}_{\mathbb{k}}(f_i)\,s$$$

Lean4

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

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