analyticAt_pi_iff — Mathlib

English

The joint map x ↦ (f_i(x)) is analytic at e if and only if each coordinate f_i is analytic at e.

Русский

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

LaTeX

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

Lean4

theorem analyticAt_pi_iff : AnalyticAt 𝕜 (fun x ↦ (f · x)) e ↔ ∀ i, AnalyticAt 𝕜 (f i) e :=
  by
  simp_rw [← analyticWithinAt_univ]
  exact analyticWithinAt_pi_iff

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