∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {x : MeasurableSpace α} [inst_3 : MeasurableSpace E] [OpensMeasurableSpace E]
  [SecondCountableTopology E] {f g : α → E}, Measurable f → Measurable g → Measurable fun t => inner 𝕜 (f t) (g t)