Exact source view. Private integrated preview.
Exact declaration: MathlibAnnex.Analysis.CStarAlgebra.Representation.cardinalMk_le_continuum_of_injective
MathlibAnnex/Analysis/CStarAlgebra/Representation/SeparableCardinality.lean · lines 22–26
1import MathlibAnnex.Analysis.Normed.Operator.Cardinality 2import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.Representation 3 4/-! # Cardinal upper bounds for faithfully separably represented algebras -/ 5set_option autoImplicit false 6open scoped Cardinal 7namespace MathlibAnnex.Analysis.CStarAlgebra 8universe u v 9variable {A : Type u} {H : Type v} 10variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 11variable [TopologicalSpace.SeparableSpace H] 12 13/-- A faithful ordinary representation on a separable Hilbert space bounds 14the cardinality of the possibly nonunital source algebra by the continuum. -/ 15theorem NonUnitalCStarRepresentation.cardinalMk_le_continuum_of_injective 16 [NonUnitalCStarAlgebra A] (pi : NonUnitalCStarRepresentation A H) 17 (hpi : Function.Injective pi) : #A ≤ Cardinal.continuum := 18 MathlibAnnex.Topology.cardinalMk_le_continuum_of_injective pi hpi 19 (MathlibAnnex.cardinalMk_continuousLinearMap_le_continuum H) 20 21/-- The unital counterpart of the faithful separable-representation bound. -/ 22theorem Representation.cardinalMk_le_continuum_of_injective 23 [CStarAlgebra A] (pi : Representation A H) (hpi : Function.Injective pi) : 24 #A ≤ Cardinal.continuum := 25 NonUnitalCStarRepresentation.cardinalMk_le_continuum_of_injective 26 pi.toNonUnitalStarAlgHom hpi 27 28end MathlibAnnex.Analysis.CStarAlgebra