Theorems · Theorem · functional analysis

isBoundedBilinearMap_inner

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E], IsBoundedBilinearMap ℝ fun p => inner 𝕜 p.1 p.2

When an inner product space E over 𝕜 is considered as a real normed space, its inner product satisfies IsBoundedBilinearMap. In order to state these results, we need a NormedSpace ℝ E instance. We will later establish such an instance by restriction-of-scalars, InnerProductSpace.rclikeToReal 𝕜 E, but this instance may be not definitionally equal to some other “natural” instance. So, we assume [NormedSpace ℝ E].

Defined in

Mathlib.Analysis.InnerProductSpace.Continuous

Cited by

6 results in Mathlib

Foundations

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

Assumes

RCLikeSeminormedAddCommGroupInnerProductSpaceNormedSpaceIsScalarTower