currying a continuous bilinear map to continuous linear map?

Stream: Is there code for X?

[Dominic Steinitz]

I’m working with a Riemannian metric g(i,p,v,w) and would like to express

$v \mapsto (w \mapsto g(i,p,v,w))$

as a ContinuousLinearMap.

In other words, I’m looking for a lemma of the form

(B : E × F → G) (hB : Continuous B) (hlin : Bilinear B) →
  ContinuousLinearMap 𝕜 E (E →L[𝕜] G)

or something equivalent to
“the currying of a continuous bilinear map is a continuous linear map.”

Does such a result already exist in mathlib (maybe under a different name)?
If not, is there an idiomatic way to construct it?

[Jireh Loreaux]

docs#IsBoundedBilinearMap.toContinuousLinearMap does this

[Jireh Loreaux]

If you have more than two variables, then you'll want something of the ContinuousMultilinearMap.curry*** variety.

[Yury G. Kudryashov]

Another approach is to use curried versions right away.

[Sébastien Gouëzel]

Normally, a Riemannian metric in the mathlib sense should already be the curried version.

[Dominic Steinitz]

I apologise that my question was misleading . I actually have

variable (IB) in
noncomputable def g' (i p : B) : TangentSpace IB p → TangentSpace IB p → ℝ := fun v w ↦
  letI dψ := mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p
  @Inner.inner ℝ EB _ (dψ v) (dψ w)

See here for the context.

Typing all this on a phone is somewhat painful - I will have access to a computer on Tuesday.

My thinking was to prove uncurried continuity to get the desired continuity. The theorem to which @Jireh Loreaux pointed me should do this.

[Dominic Steinitz]

But I just discovered

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/
InnerProductSpace/LinearMap.html

So I think I just have to define my function as

def g_bilin (i : ι) (p : B) :
    TangentSpace IB i →L[ℝ] (TangentSpace IB i →L[ℝ] ℝ) :=
  let dψ := mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p
  innerSL ℝ EB |>.comp dψ |>.flip.comp dψ