Theorems · Theorem · functional analysis

WithCStarModule.norm_apply_le_norm

∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] [StarOrderedRing A]
  (x : WithCStarModule A ((i : ι) → E i)) (i : ι), ‖x i‖ ≤ ‖x‖

Defined in

Mathlib.Analysis.CStarAlgebra.Module.Constructions

Cited by

2 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraPartialOrderFintypeNormedAddCommGroupModuleSMulCStarModuleStarOrderedRing