Theorems · Theorem · functional analysis

Continuous.inner

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {α : Type u_4} [inst_3 : TopologicalSpace α] {f g : α → E},
  Continuous f → Continuous g → Continuous fun t => inner 𝕜 (f t) (g t)

Defined in

Mathlib.Analysis.InnerProductSpace.Continuous

Cited by

19 results in Mathlib

Foundations

Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeSeminormedAddCommGroupInnerProductSpaceTopologicalSpace