Theorems · Theorem · functional analysis

ContinuousLinearMap.norm_precompR_le

∀ {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup Eₗ] [inst_2 : SeminormedAddCommGroup Fₗ] [inst_3 : SeminormedAddCommGroup Gₗ]
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 E] [inst_6 : NormedSpace 𝕜 Eₗ]
  [inst_7 : NormedSpace 𝕜 Fₗ] [inst_8 : NormedSpace 𝕜 Gₗ] (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ),
  ‖ContinuousLinearMap.precompR Eₗ L‖ ≤ ‖L‖

Defined in

Mathlib.Analysis.Normed.Operator.Bilinear

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroupNontriviallyNormedFieldNormedSpaceNormedSpaceNormedSpaceNormedSpace