analyticOnNhd_pi_iff — Mathlib

English

AnalyticOnNhd of the joint map is equivalent to analyticOn of each coordinate.

Русский

Аналитичность в окрестности совместного отображения равносильна аналитичности каждой координаты.

LaTeX

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

Lean4

theorem analyticOnNhd_pi_iff : AnalyticOnNhd 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticOnNhd 𝕜 (f i) s :=
  ⟨fun h i x hx ↦ analyticAt_pi_iff.1 (h x hx) i, fun h ↦ .pi h⟩

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