analyticOnNhd_uncurry_compContinuousLinearMap

English

The analytic at point x version holds for the uncurry of a linear construction.

Русский

Утверждается аналитичность в точке x для распакованной линейной конструкции.

LaTeX

$$$AnalyticAt_{\mathbb{k}}(p \mapsto f(p_1)(p_2))\, x$$$

Lean4

theorem analyticOnNhd_uncurry_compContinuousLinearMap :
    AnalyticOnNhd 𝕜
      (fun (p : (Π i, Fm i →L[𝕜] Em i) × (ContinuousMultilinearMap 𝕜 Em G)) ↦ p.2.compContinuousLinearMap p.1) t :=
  analyticOnNhd_uncurry_of_linear (ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 Fm Em G)

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