English
There exists a unique continuous monoid isomorphism between two monoids with a single element; i.e., if M and N have unique elements, then there is a unique ContinuousMulEquiv M ≃ₜ* N.
Русский
Существует единственная непрерывная моноидная изоморфия между двумя моноидами с единственным элементом; то есть если M и N имеют уникальные элементы, то существует единственный ContinuousMulEquiv M ≃ₜ* N.
LaTeX
$$$\exists! e : M \simeq_{\mathrm{top}}^* N$ under the assumptions of uniqueness for M and N$$
Lean4
/-- The `MulEquiv` between two monoids with a unique element. -/
@[to_additive /-- The `AddEquiv` between two `AddMonoid`s with a unique element. -/
]
def ofUnique {M N} [Unique M] [Unique N] [Mul M] [Mul N] [TopologicalSpace M] [TopologicalSpace N] : M ≃ₜ* N
where
__ := MulEquiv.ofUnique
continuous_toFun := by continuity
continuous_invFun := by continuity
