English
The joint map x ↦ (f_i(x)) is analytic at e iff every coordinate f_i is analytic at e.
Русский
Совместное отображение x ↦ (f_i(x)) аналитично в e тогда и только тогда, когда каждая f_i аналитична в e.
LaTeX
$$$\text{AnalyticAt}_{\mathbb{k}}(\lambda x. (f \cdot x))\,e \iff \forall i, \text{AnalyticAt}_{\mathbb{k}}(f_i)\,e$$$
Lean4
/-- Scalar multiplication is analytic (jointly in both variables). The statement is a little
pedantic to allow towers of field extensions.
TODO: can we replace `𝕜'` with a "normed module" in such a way that `analyticAt_mul` is a special
case of this? -/
@[fun_prop]
theorem analyticAt_smul [NormedSpace 𝕝 E] [IsScalarTower 𝕜 𝕝 E] (z : 𝕝 × E) :
AnalyticAt 𝕜 (fun x : 𝕝 × E ↦ x.1 • x.2) z :=
(ContinuousLinearMap.lsmul 𝕜 𝕝).analyticAt_bilinear z
