English
If a type F consists of objects that are both monoid homomorphisms A → B and continuous maps A → B, then every f : F determines a continuous monoid homomorphism from A to B.
Русский
Если тип F состоит из элементов, которые одновременно являются моноид-гомоморфизмами A → B и непрерывными отображениями A → B, то каждый элемент f : F задаёт непрерывный моноид-гомоморфизм A →* B.
LaTeX
$$$toContinuousMonoidHom(f)\\in A \\to_{}^{\\mathrm{t}}_* B$$$
Lean4
/-- Turn an element of a type `F` satisfying `MonoidHomClass F A B` and `ContinuousMapClass F A B`
into a`ContinuousMonoidHom`. This is declared as the default coercion from `F` to
`(A →ₜ* B)`. -/
@[to_additive (attr := coe) /-- Turn an element of a type `F` satisfying
`AddMonoidHomClass F A B` and `ContinuousMapClass F A B` into a`ContinuousAddMonoidHom`.
This is declared as the default coercion from `F` to `ContinuousAddMonoidHom A B`. -/
]
def toContinuousMonoidHom [MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : A →ₜ* B :=
{ MonoidHomClass.toMonoidHom f with }
