Documentation

LeanAPAP.Mathlib.Topology.Algebra.Group.CompactOpen

source
theorem ContinuousMonoidHom.isClosedEmbedding_coe {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] [TopologicalSpace M] [TopologicalSpace N] [DiscreteTopology M] [ContinuousMul N] [T2Space N] :
Topology.IsClosedEmbedding DFunLike.coe
source
theorem ContinuousAddMonoidHom.isClosedEmbedding_coe {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] [TopologicalSpace M] [TopologicalSpace N] [DiscreteTopology M] [ContinuousAdd N] [T2Space N] :
Topology.IsClosedEmbedding DFunLike.coe
source
instance ContinuousMonoidHom.instCompactSpace_leanAPAP {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] [TopologicalSpace M] [TopologicalSpace N] [DiscreteTopology M] [ContinuousMul N] [T2Space N] [CompactSpace N] :
CompactSpace (M →ₜ* N)
source
instance ContinuousAddMonoidHom.instCompactSpace_leanAPAP {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] [TopologicalSpace M] [TopologicalSpace N] [DiscreteTopology M] [ContinuousAdd N] [T2Space N] [CompactSpace N] :
CompactSpace (M →ₜ+ N)