Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/SeparableCardinality.lean
Pinned GitHub source · Raw UTF-8 source
Back to Exact norm density of the fixed atomic algebra
1import MathlibAnnex.Analysis.Normed.Operator.Cardinality2import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.Representation34/-! # Cardinal upper bounds for faithfully separably represented algebras -/5set_option autoImplicit false6open scoped Cardinal7namespace MathlibAnnex.Analysis.CStarAlgebra8universe u v9variable {A : Type u} {H : Type v}10variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]11variable [TopologicalSpace.SeparableSpace H]1213/-- A faithful ordinary representation on a separable Hilbert space bounds14the cardinality of the possibly nonunital source algebra by the continuum. -/15theorem NonUnitalCStarRepresentation.cardinalMk_le_continuum_of_injective16 [NonUnitalCStarAlgebra A] (pi : NonUnitalCStarRepresentation A H)17 (hpi : Function.Injective pi) : #A ≤ Cardinal.continuum :=18 MathlibAnnex.Topology.cardinalMk_le_continuum_of_injective pi hpi19 (MathlibAnnex.cardinalMk_continuousLinearMap_le_continuum H)2021/-- The unital counterpart of the faithful separable-representation bound. -/22theorem Representation.cardinalMk_le_continuum_of_injective23 [CStarAlgebra A] (pi : Representation A H) (hpi : Function.Injective pi) :24 #A ≤ Cardinal.continuum :=25 NonUnitalCStarRepresentation.cardinalMk_le_continuum_of_injective26 pi.toNonUnitalStarAlgHom hpi2728end MathlibAnnex.Analysis.CStarAlgebra