analyticOn_pi_iff — Mathlib

English

AnalyticOn of the joint map x ↦ (f_i(x)) on s is equivalent to analyticOn of each coordinate f_i on s.

Русский

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

LaTeX

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

Lean4

theorem analyticOn_pi_iff : AnalyticOn 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticOn 𝕜 (f i) s :=
  ⟨fun h i x hx ↦ analyticWithinAt_pi_iff.1 (h x hx) i, fun h ↦ .pi h⟩

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