Exact source: MathlibAnnex/Analysis/CStarAlgebra/Generated.lean, lines 14–15.
Back to The closed operator algebra generated by a representation and extra operators
1import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap 2import Mathlib.Topology.Algebra.StarSubalgebra 3 4/-! Concrete norm-closed star algebra generated by specified operators. -/ 5 6set_option autoImplicit false 7 8namespace MathlibAnnex.Analysis.CStarAlgebra 9 10variable {H : Type*} 11variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 12 13/-- The norm-closed unital star subalgebra generated by a set of operators. -/ 14noncomputable def generated (S : Set (H →L[ℂ] H)) : StarSubalgebra ℂ (H →L[ℂ] H) := 15 (StarAlgebra.adjoin ℂ S).topologicalClosure 16 17/-- Every nominated generator belongs to the generated C*-subalgebra. -/ 18theorem subset_generated (S : Set (H →L[ℂ] H)) : S ⊆ generated S := 19 fun _ hT ↦ StarSubalgebra.le_topologicalClosure _ (StarAlgebra.subset_adjoin ℂ S hT) 20 21/-- The generated star subalgebra is norm closed. -/ 22theorem isClosed_generated (S : Set (H →L[ℂ] H)) : 23 IsClosed (generated S : Set (H →L[ℂ] H)) := 24 StarSubalgebra.isClosed_topologicalClosure _ 25 26end MathlibAnnex.Analysis.CStarAlgebra