Separately continuous multiplication on subgroups #
A subgroup of a group with separately continuous multiplication has separately continuous multiplication for the subspace topology. Mathlib provides this for submonoids, but instance search does not see a subgroup as a submonoid, so the subgroup instance is registered separately.
Main results #
Subgroup.separatelyContinuousMul: a subgroup inheritsSeparatelyContinuousMul.
instance
Subgroup.separatelyContinuousMul
{G : Type u_1}
[TopologicalSpace G]
[Group G]
[SeparatelyContinuousMul G]
(S : Subgroup G)
:
A subgroup of a group with separately continuous multiplication has separately continuous multiplication.
instance
AddSubgroup.separatelyContinuousAdd
{G : Type u_1}
[TopologicalSpace G]
[AddGroup G]
[SeparatelyContinuousAdd G]
(S : AddSubgroup G)
:
An additive subgroup of an additive group with separately continuous addition has separately continuous addition.