analyticOn_uncurry_compContinuousLinearMap

English

The function p ↦ p.2.compContinuousLinearMap p.1 is analytic on the space of pairs (p1, p2).

Русский

Функция p ↦ p.2.compContinuousLinearMap p.1 аналитична на парном пространстве.

LaTeX

$$$AnalyticOn\ 𝕜\ (\lambda p \mapsto p.2.compContinuousLinearMap p.1)\ t$$$

Lean4

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

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