Theorems · Theorem · functional analysis

WithCStarModule.prod_norm_le_norm_add

∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {E : Type u_2} {F : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : SMul A F] [inst_8 : CStarModule A E] [inst_9 : CStarModule A F]
  (x : WithCStarModule A (E × F)), ‖x‖ ≤ ‖x.1‖ + ‖x.2‖

Defined in

Mathlib.Analysis.CStarAlgebra.Module.Constructions

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraPartialOrderNormedAddCommGroupModuleSMulNormedAddCommGroupModuleSMulCStarModuleCStarModule