import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
import Mathlib.Topology.Algebra.StarSubalgebra

/-! Concrete norm-closed star algebra generated by specified operators. -/

set_option autoImplicit false

namespace MathlibAnnex.Analysis.CStarAlgebra

variable {H : Type*}
variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

/-- The norm-closed unital star subalgebra generated by a set of operators. -/
noncomputable def generated (S : Set (H →L[ℂ] H)) : StarSubalgebra ℂ (H →L[ℂ] H) :=
  (StarAlgebra.adjoin ℂ S).topologicalClosure

/-- Every nominated generator belongs to the generated C*-subalgebra. -/
theorem subset_generated (S : Set (H →L[ℂ] H)) : S ⊆ generated S :=
  fun _ hT ↦ StarSubalgebra.le_topologicalClosure _ (StarAlgebra.subset_adjoin ℂ S hT)

/-- The generated star subalgebra is norm closed. -/
theorem isClosed_generated (S : Set (H →L[ℂ] H)) :
    IsClosed (generated S : Set (H →L[ℂ] H)) :=
  StarSubalgebra.isClosed_topologicalClosure _

end MathlibAnnex.Analysis.CStarAlgebra