Applying continuous linear map

Stream: Is there code for X?

[Patrick Massot]

I can't find:

variables
      (𝕜 : Type*)  (E : Type*) (F : Type*) [normed_group E]
      [normed_group F] [nondiscrete_normed_field 𝕜]
      [normed_space 𝕜 E] [normed_space 𝕜 F]

def continuous_linear_map.uncurry_apply : (E →L[𝕜] F) × E → F :=
λ p, p.1 p.2

lemma continuous_linear_map.is_bounded_bilinear_uncurry_apply :
  is_bounded_bilinear_map 𝕜 (continuous_linear_map.uncurry_apply 𝕜 E F) :=
{ add_left := λ x φ ψ, continuous_linear_map.add_apply _ _ _,
  smul_left := λ s x φ, rfl,
  add_right := λ φ x y, φ.map_add x y,
  smul_right := λ s φ x, φ.map_smul s x,
  bound := ⟨1, zero_lt_one, λ φ x, by simpa using φ.le_op_norm x⟩ }

Where is it hidden?

[Patrick Massot]

Note that I found docs#continuous_linear_map.apply, but I didn't know how to convert it to the above.

[Heather Macbeth]

I think this is docs#is_bounded_bilinear_map_apply, right?

[Patrick Massot]

Yes!

[Patrick Massot]

Thanks!