Theorems · Theorem · functional analysis

ContinuousLinearMap.norm_compL_le

∀ (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) (Gₗ : Type u_9) [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup Fₗ] [inst_2 : SeminormedAddCommGroup Gₗ] [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 Fₗ] [inst_6 : NormedSpace 𝕜 Gₗ],
  ‖ContinuousLinearMap.compL 𝕜 E Fₗ Gₗ‖ ≤ 1

Defined in

Mathlib.Analysis.Normed.Operator.Bilinear

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroupNontriviallyNormedFieldNormedSpaceNormedSpaceNormedSpace