cpolynomialAt_uncurry_compContinuousLinearMap

English

The nhd-analyticity holds for the uncurried map with continuous linear map composition.

Русский

Утверждается аналитичность по окрестности для распакованной карты с композициями непрерывных линейных отображений.

LaTeX

$$$AnalyticOnNhd_{\mathbb{k}}\bigl(p \mapsto ContinuousLinearMap.coe(ContinuousMultilinearMap.coe f\,p_{\text{fst}})\, p_{\text{snd}}\bigr)\, s$$$

Lean4

theorem cpolynomialAt_uncurry_compContinuousLinearMap :
    CPolynomialAt 𝕜
      (fun (p : (Π i, Fm i →L[𝕜] Em i) × (ContinuousMultilinearMap 𝕜 Em G)) ↦ p.2.compContinuousLinearMap p.1) q :=
  cpolynomialAt_uncurry_of_linear (ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 Fm Em G)

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