Exact source: MathlibAnnex/Analysis/CStarAlgebra/Generated.lean
Pinned GitHub source · Raw UTF-8 source
Back to The closed operator algebra generated by a representation and extra operators
1import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap2import Mathlib.Topology.Algebra.StarSubalgebra34/-! Concrete norm-closed star algebra generated by specified operators. -/56set_option autoImplicit false78namespace MathlibAnnex.Analysis.CStarAlgebra910variable {H : Type*}11variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]1213/-- 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).topologicalClosure1617/-- 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)2021/-- 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 _2526end MathlibAnnex.Analysis.CStarAlgebra