Topological properties of the unitary (sub)group

• In a topological star monoid R, unitary R is a topological group
• In a topological star monoid R which is T1, unitary R is closed as a subset of R.

instance instContinuousStarSubtypeMemSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] [TopologicalSpace R] [ContinuousStar R] : ContinuousStar ↥(unitary R)

instance instContinuousInvSubtypeMemSubmonoidUnitaryOfContinuousStar {R : Type u_1} [Monoid R] [StarMul R] [TopologicalSpace R] [ContinuousStar R] : ContinuousInv ↥(unitary R)

instance instIsTopologicalGroupSubtypeMemSubmonoidUnitaryOfContinuousMulOfContinuousStar {R : Type u_1} [Monoid R] [StarMul R] [TopologicalSpace R] [ContinuousMul R] [ContinuousStar R] : IsTopologicalGroup ↥(unitary R)

theorem isClosed_unitary {R : Type u_1} [Monoid R] [StarMul R] [TopologicalSpace R] [T1Space R] [ContinuousStar R] [ContinuousMul R] : IsClosed ↑(unitary R)